packages feed

Agda-2.3.2.2: src/prototyping/nameless/Main.hs

module Main where

import Control.Applicative
import System.Environment

import Lam.Par
import Lam.Lex
import Lam.Layout
import Lam.Abs
import Lam.ErrM
import Lam.Print

import Syntax
import TypeChecker
import Stack

parse :: String -> Err Prog
parse s = pProg $ resolveLayout True $ myLexer s

parseFile :: FilePath -> IO (Err Prog)
parseFile file = parse <$> readFile file

goFile :: FilePath -> IO ()
goFile file = do
  r <- parseFile file
  case r of
    Bad err -> putStrLn $ "Error:\n" ++ err
    Ok p    -> do
      print p
      putStrLn "--- Type checked ---"
      case runTCM emptyEnv $ checkProgram p of
        Left err -> putStrLn $ "ERROR:\n" ++ err
        Right ds -> mapM_ (putStrLn . printTree . toAbstractDecl) ds

main = do
  args <- getArgs
  case args of
    [file]  -> goFile file
    _       -> putStrLn "File argument missing."