packages feed

HaRe-0.6: tools/pg2hol/Main.hs

-- $Id: Main.hs,v 1.5 2001/10/10 23:43:23 hallgren Exp $

-- Currently a test harness for lexer/parser/pretty printer/prop2hol.

module Main (main) where


import IO
import Lexer
import ParseMonad
import PropParser
import ParseUtil
import Syntax
import PrettyPrint
import System
import GetOpt
import IOExts
import List
import Rewrite(rewriteModule)
import HsAssocInitEnv(initEnv)
import Prop2HOL(prop2HOL)


data Flag = LexOnlyLength          -- print number of tokens only
          | LexOnlyRev             -- print tokens in reverse order
          | LexOnly                -- print tokens
          | ParseLength            -- print number of declarations only
          | ParseInternal          -- print abstract syntax in internal format
          | ParsePretty PPLayout   -- pretty print in this style
          | ToHOL                  -- produces naive HOL version
          | TestStatic             -- test static checker
          | TestTypeCheck
          | ShowNames
          | Help                   -- give short usage info

usage = "usage: prop2hol [option] [filename]"

options =
   [ Option ['n']  ["numtokens"] (NoArg LexOnlyLength)
         "print number of tokens only",
     Option ['r']  ["revtokens"] (NoArg LexOnlyRev)
         "print tokens in reverse order",
     Option ['t']  ["tokens"]    (NoArg LexOnly)
         "print tokens",
     Option ['d']  ["numdecls"]  (NoArg ParseLength)
         "print number of declarations only",
     Option ['a']  ["abstract"]  (NoArg ParseInternal)
         "print abstract syntax in internal format",
     Option ['p']  ["pretty"]    (OptArg style "STYLE")
         "pretty print in STYLE[(o)ffside|(s)emicolon|(u)trecht|(i)nline|\
                    \(n)one] (default = offside)",
     Option ['h','?'] ["help"]   (NoArg Help)
         "display this help and exit",
     Option ['s'] ["static"] (NoArg TestStatic) 
         "run stattic checker",
     Option ['c'] ["typecheck"] (NoArg TestTypeCheck) "run typechecker",
     Option ['m'] ["names"]     (NoArg ShowNames)      "show all defined names"
   ]

style :: Maybe String -> Flag
style Nothing  = ToHOL
style (Just s) = ParsePretty $
         case s of
         "o"         -> PPOffsideRule
         "offside"   -> PPOffsideRule
         "s"         -> PPSemiColon
         "semicolon" -> PPSemiColon
         "u"         -> PPUtrecht
         "utrecht  " -> PPUtrecht
         "i"         -> PPInLine
         "inline"    -> PPInLine
         "n"         -> PPNoLayout
         "none"      -> PPNoLayout
         _           -> PPOffsideRule

main :: IO ()
main = do cmdline <- getArgs
          mainHugs cmdline

mainHugs :: [String] -> IO ()
mainHugs cmdline =
   case getOpt Permute options cmdline of
      (flags, args, [])    ->
       do (file, inp) <- case args of
			 []  -> do inp <- getContents
				   return ("stdio", inp)
			 [f] -> do inp <- readFile f
				   return (f, inp)
			 _   -> error usage
          putStrLn (handleFlag (getFlag flags) file inp)
      (    _,   _, errors) ->
        error (concat errors ++ usageInfo usage options)

getFlag :: [Flag] -> Flag
getFlag []  = ToHOL
getFlag [f] = f
getFlag _   = error usage

handleFlag :: Flag -> FilePath -> String -> String
handleFlag LexOnlyLength    f = show . numToks . testLexerRev f
handleFlag LexOnlyRev       f = show . testLexerRev f
handleFlag LexOnly          f = show . testLexer f
handleFlag ShowNames        f = 
    error "Main.handleFlag: name extraction not implemented yet."
-- show . getAllNames . testParser f
handleFlag ParseLength      f = show . allLengths . testParser f
   where allLengths (HsModule _ _ imp d) =
            length imp + length d
handleFlag ParseInternal    f = show . testParser f
handleFlag ToHOL            f = render . testProp2HOL f
handleFlag TestStatic       f =
    error "Main.handleFlag: static analysis test not implemented yet."
{-
handleFlag TestStatic       f = \s -> 
    unsafePerformIO $ 
    do { r <- testStatic $ testParser f s ;
         return "Done static checking." }
-}
handleFlag TestTypeCheck    f =
    error "Main.handleFlag: type check test not implemented yet."
{-
handleFlag TestTypeCheck    f = \s -> 
    unsafePerformIO $ 
    do  { let { m = testParser f s } ;
          r <- testStatic m ;
          print $ (typeCheckDecls . (\ (HsModule _ _ _ _ ds) -> ds)) m;
          return "Done static checking." }
-}
handleFlag (ParsePretty lo) f
    = renderWithMode mode . ppi . testParser f
      where mode = defaultMode { layoutType = lo }
handleFlag Help             f          
    = const $
      usageInfo
          ("A simple test program for *The Haskell Parser*" ++ usage)
      options

numToks :: ParseResult () [Token] -> Int
numToks (Ok _ toks)  = length toks
numToks (Failed err) = error ("Huh? " ++ err)

testLexerRev :: FilePath -> String -> ParseResult () [Token]
testLexerRev f s =
    (unPM $ loop []) s (SrcLoc f 1 0) 1 (error "Initial environment", []) 
    where loop toks =
	      lexer (\t -> case t of 
                           EOF -> returnPM toks
                           _   -> loop (t:toks))

testLexer :: FilePath -> String -> ParseResult () [Token]
testLexer f s = (unPM $ loop []) s  (SrcLoc f 1 0) 1 ((), [])
  where loop toks =
         lexer (\t -> case t of 
              EOF -> returnPM (reverse toks) -- space leak?
              _   -> loop (t:toks))

testParser :: FilePath -> String -> HsModuleR
testParser f s =
    case (unPM parse) s  (SrcLoc f 1 1) 0 ((), []) of
    Ok state mod -> rewriteModule initEnv mod
    Failed err -> error err

testProp2HOL f s = prop2HOL $ testParser f s

------------------------------------------------------------------------------
-- tests
--

n = UnQual 
loc = SrcLoc "MyFile" 1 1
{-
t1 :: HsDecl
t1 = hsDataDecl loc []
        {-data-} [hsTyCon $ n "List", hsTyVar $ n "a"]
        [ HsConDecl loc (n "Nil") []
        , HsConDecl loc (n "Cons")
            [ HsUnBangedType (hsTyVar $ n "a")
            , HsUnBangedType (hsTyApp (hsTyCon $ n "List") (hsTyVar $n "a"))
            ]
        ]
        {-deriving-} []
-}
----------------------------------------------------------------------------