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 :: IO ()
main = do
  Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdout BufferMode
NoBuffering
  -- putStrLn "MiniAgda by Andreas Abel and Karl Mehltretter"
  opts <- IO Options
options
  mapM_ mainFile $ optInputs opts

mainFile :: String -> IO ()
mainFile :: String -> IO ()
mainFile String
fileName = do
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"--- opening " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
fileName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ---"
  file <- String -> IO String
readFile String
fileName
  let t = String -> [Token]
alexScanTokens String
file
  let cdecls =  [Token] -> [Declaration]
parse [Token]
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 :: PPHsMode
ppHsMode = H.PPHsMode  -- H.defaultMode
  { classIndent :: Indent
H.classIndent  = Indent
2
  , doIndent :: Indent
H.doIndent     = Indent
3
  , multiIfIndent :: Indent
H.multiIfIndent = Indent
3
  , caseIndent :: Indent
H.caseIndent   = Indent
3
  , letIndent :: Indent
H.letIndent    = Indent
4
  , whereIndent :: Indent
H.whereIndent  = Indent
2
  , onsideIndent :: Indent
H.onsideIndent = Indent
1
  , spacing :: Bool
H.spacing      = Bool
False
  , layout :: PPLayout
H.layout       = PPLayout
H.PPOffsideRule
  , linePragmas :: Bool
H.linePragmas  = Bool
False
  }

printHsDecls :: [H.Decl ()] -> IO ()
printHsDecls :: [Decl ()] -> IO ()
printHsDecls [Decl ()]
hs = (Decl () -> IO ()) -> [Decl ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> (Decl () -> String) -> Decl () -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PPHsMode -> Decl () -> String
forall a. Pretty a => PPHsMode -> a -> String
H.prettyPrintWithMode PPHsMode
ppHsMode) [Decl ()]
hs

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


showAll :: Signature -> [A.Declaration] -> IO ()
showAll :: Signature -> [Declaration] -> IO ()
showAll Signature
sig [Declaration]
decl = ((Name, Expr) -> IO ()) -> [(Name, Expr)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Signature -> (Name, Expr) -> IO ()
showLet Signature
sig) ([(Name, Expr)] -> IO ()) -> [(Name, Expr)] -> IO ()
forall a b. (a -> b) -> a -> b
$ Signature -> [Declaration] -> [(Name, Expr)]
allLet Signature
sig [Declaration]
decl

showLet :: Signature -> (Name,A.Expr) -> IO ()
showLet :: Signature -> (Name, Expr) -> IO ()
showLet Signature
sig (Name
n,Expr
e) = do
  r <- Signature -> Expr -> IO (Either TraceError (Val, TCState))
doWhnf Signature
sig Expr
e
  case r of
    Right (Val
v,TCState
_) -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has whnf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Val -> String
forall a. Show a => a -> String
show Val
v
    Left TraceError
err    -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"error during evaluation:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TraceError -> String
forall a. Show a => a -> String
show TraceError
err
                      IO ()
forall a. IO a
exitFailure
  r <- doNf sig e
  case r of
    Right (Expr
v,TCState
_) -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" evaluates to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
v
    Left TraceError
err    -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"error during evaluation:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TraceError -> String
forall a. Show a => a -> String
show TraceError
err
                      IO ()
forall a. IO a
exitFailure

doExtract :: Signature -> [A.EDeclaration] -> IO [A.EDeclaration]
doExtract :: Signature -> [Declaration] -> IO [Declaration]
doExtract Signature
sig [Declaration]
decls = do
  k <- Signature
-> TypeCheck [Declaration]
-> IO (Either TraceError ([Declaration], TCState))
forall a.
Signature -> TypeCheck a -> IO (Either TraceError (a, TCState))
runExtract Signature
sig (TypeCheck [Declaration]
 -> IO (Either TraceError ([Declaration], TCState)))
-> TypeCheck [Declaration]
-> IO (Either TraceError ([Declaration], TCState))
forall a b. (a -> b) -> a -> b
$ [Declaration] -> TypeCheck [Declaration]
extractDecls [Declaration]
decls
  case k of
    Left TraceError
err -> do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"error during extraction:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TraceError -> String
forall a. Show a => a -> String
show TraceError
err
      IO [Declaration]
forall a. IO a
exitFailure
    Right ([Declaration]
hs, TCState
_) ->
      [Declaration] -> IO [Declaration]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Declaration]
hs

doTranslate :: [A.EDeclaration] -> IO (H.Module ())
doTranslate :: [Declaration] -> IO (Module ())
doTranslate [Declaration]
decls = do
  k <- Translate (Module ()) -> IO (Either TraceError (Module ()))
forall a. Translate a -> IO (Either TraceError a)
runTranslate (Translate (Module ()) -> IO (Either TraceError (Module ())))
-> Translate (Module ()) -> IO (Either TraceError (Module ()))
forall a b. (a -> b) -> a -> b
$ [Declaration] -> Translate (Module ())
translateModule [Declaration]
decls
  case k of
    Left TraceError
err -> do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"error during extraction:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TraceError -> String
forall a. Show a => a -> String
show TraceError
err
      IO (Module ())
forall a. IO a
exitFailure
    Right Module ()
hs ->
      Module () -> IO (Module ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Module ()
hs

doTypeCheck :: [A.Declaration] -> IO ([A.EDeclaration], Signature)
doTypeCheck :: [Declaration] -> IO ([Declaration], Signature)
doTypeCheck [Declaration]
decls = do
  k <- [Declaration] -> IO (Either TraceError ([Declaration], TCState))
typeCheck [Declaration]
decls
  case k of
    Left TraceError
err -> do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"error during typechecking:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TraceError -> String
forall a. Show a => a -> String
show TraceError
err
      IO ([Declaration], Signature)
forall a. IO a
exitFailure
    Right ([Declaration]
edecls, TCState
st) ->
      ([Declaration], Signature) -> IO ([Declaration], Signature)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Declaration]
edecls, TCState -> Signature
signature TCState
st)

doScopeCheck :: [C.Declaration] -> IO [A.Declaration]
doScopeCheck :: [Declaration] -> IO [Declaration]
doScopeCheck [Declaration]
decl = case [Declaration] -> Either TraceError ([Declaration], SCState)
scopeCheck [Declaration]
decl of
     Left TraceError
err -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"scope check error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TraceError -> String
forall a. Show a => a -> String
show TraceError
err
                    IO [Declaration]
forall a. IO a
exitFailure
     Right ([Declaration]
decl',SCState
_) -> [Declaration] -> IO [Declaration]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Declaration] -> IO [Declaration])
-> [Declaration] -> IO [Declaration]
forall a b. (a -> b) -> a -> b
$ [Declaration]
decl'