{-|

Module : $Header$

Copyright : (c) Felix Reckers, Uni Bremen 2002-2004

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : provisional

Portability : portable

-}

module Main where

import System.Console.GetOpt

import System.Directory

import System

import Parsec

import Common.Utils

import ParseFile

import ParseHeader

data Flag = Rule String | Exclude String | Header String

| Output_Directory String deriving Show

options :: [OptDescr Flag]

options = [

Option ['r'] ["rule"] (ReqArg Rule "RULE")

"rules are the actual DrIFT derivations",

Option ['x'] ["exclude"] (ReqArg Exclude "data[:data]")

"excludes the specified data-types",

Option ['h'] ["header"] (ReqArg Header "FILE[:FILE]")

"uses the header-file(s) for generation, parses them and ommites the rules for the instances in the header(s)",

Option ['o'] ["output-directory"] (ReqArg Output_Directory "DIR")

"specifies the output-directory"

]

main :: IO ()

main = do args <- getArgs

case (getOpt RequireOrder options args) of

(m,n,[]) -> case n of

[] -> ioError $ userError ("no filename specified\n"

++ usageInfo header options)

fs -> genRules m fs

(_,_,errs) -> ioError (userError (concat errs

++ usageInfo header options))

where header = "Usage: genRules [OPTION...] file [file ...]"

genRules :: [Flag] -> [FilePath] -> IO ()

genRules flags files = do inp <- mapM readFile files

(ds,imports) <- case (parse inputFile ""

(concat inp)) of

Left err -> do putStr "parse error at "

print err;return ([],[])

Right x -> return x

(rule,dir) <- getRuleAndDir flags

fps <- getPaths flags

headers <- mapM readFile fps

exc <- parseHeader (concat headers)

ds' <- exclude flags exc ds

imports' <- checkImports (fileWP dir)

("Common.ATerm.Lib":imports)

writeFile (dir ++"/"++fileWP dir++".der.hs") $

fileHead ++ "\n\nmodule " ++ dir ++ "."

++ fileWP dir

++ " where\n\n"

++ (if dir == "CspCASL" then

"import CASL.ATC_CASL\n" else "")

++ concat (map (\x->"import "++x++"\n")

imports')

++ "\n" ++ concat headers ++ "\n"

++ rules rule ds' ++ "\n"

where

fileHead = "{-\n Generated by 'genRules' (automatic rule generation for DrIFT). Don't touch!!\n dependency files: " ++ unwords files ++"\n-}"

fileWP dir = if (firstdirname (head files)

/= (dir++"/"))

then (cutSuffix $ basename (head files))

else ("ATC_"++dir)

firstdirname :: FilePath -> FilePath

firstdirname fp = (fst $ break (== '/') fp) ++ "/"

parseHeader :: String -> IO [Exclude]

parseHeader [] = return []

parseHeader hs = case (parse header "" hs) of

Left err -> do putStrLn "parse error at "

print err

return []

Right x -> return x

checkImports :: String -> [Import] -> IO [Import]

checkImports fn xs = do imports <- return $ removeMultipleImports xs

importsATC <- return $ map (\x-> "ATC."

++ (cutModuleName x)) imports

bools <- mapM doesFileExist (map (\x->"ATC/"

++cutModuleName x++".der.hs") importsATC)

return $ checkSpecialImports fn

(imports ++ (filter (/=[])

(map selectTrue (zip bools importsATC))))

where

selectTrue :: (Bool,String) -> String

selectTrue (True,x) = x

selectTrue (False,x) = []

checkSpecialImports :: String -> [Import] -> [Import]

checkSpecialImports fn [] = []

checkSpecialImports fn (x:xs) | x == "Logic.Grothendieck" =

x : "ATC.Grothendieck" : xs

| x == "ATC."++fn = xs

| otherwise =

x : (checkSpecialImports fn xs)

removeMultipleImports :: [String] -> [String]

removeMultipleImports [] = []

removeMultipleImports (x:xs) | multi x xs = removeMultipleImports xs

| otherwise = x : (removeMultipleImports xs)

where

multi s [] = False

multi s (x:xs) | s==x = True

| s/=x = multi s xs

cutModuleName :: FilePath -> FilePath

cutModuleName fp = reverse $ remP $ fst $ break (=='.') (reverse fp)

where remP [] = []

remP xs@(x:xs1)

| x == '.' = xs1

| otherwise = xs

rules :: String -> [String] -> String

rules rule [] = []

rules rule (d:ds) = "{-! for " ++ d ++ " derive : " ++ rule ++ " !-}\n"

++ rules rule ds

exclude :: [Flag] -> [Data] -> [Data] -> IO [String]

exclude [] exc ds = return [ d | d <- ds,not (elem d exc) ]

exclude ((Exclude s):fs) exc ds =

case (parse (sepBy1 identifier (char ':')) "" s) of

Left err -> do putStr "can't parse exclude datatypes"

print err

return []

Right excs -> return [ d | d <- ds,not (elem d excs),not (elem d exc) ]

exclude (_:fs) exc ds = exclude fs exc ds

getPaths :: [Flag] -> IO [FilePath]

getPaths [] = return []

getPaths ((Header s):fs) =

case (parse (sepBy1 path (char ':')) "" s) of

Left err -> do putStr "couldn't parse header-files"

print err

return []

Right x -> return x

getPaths (_:fs) = getPaths fs

path :: Parser FilePath

path = many1 (noneOf ":*+?<>")

dirName :: Parser String

dirName = many1 (noneOf "/*+?<>")

getRuleAndDir :: [Flag] -> IO (String,String)

getRuleAndDir flags = return (getRule flags,getDir flags)

where

getRule ((Rule s):_) = s

getRule (_:xs) = getRule xs

getDir ((Output_Directory s):_) = s

getDir (_:xs) = getDir xs

cutSuffix :: String -> String

cutSuffix f = cutS "" f

where

cutS s ('.':_) = s

cutS s (x:xs) = cutS (s++ [x]) xs