a945f35eff8b6a88009ce73de6d4c862ce58de3cslive{- |

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveModule : $Header$

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveCopyright : (c) Christian Maeder, Uni Bremen 2002-2005

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveMaintainer : meader@tzi.de

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveStability : experimental

a945f35eff8b6a88009ce73de6d4c862ce58de3cslivePortability : non-portable(uses programatica)

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive

06ba4a61654b3763ad65f52283832ebf058fdf1cslivetest translation from Haskell to Isabelle

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive-}

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slivemodule Main where

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport System.Environment

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Data.Char

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveimport Text.ParserCombinators.Parsec

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveimport Common.Result

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Common.AnnoState

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Common.AS_Annotation

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Common.GlobalAnnotations

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Comorphisms.Hs2HOLCF

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport Isabelle.IsaPrint

06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport Isabelle.IsaSign as IsaSign

06ba4a61654b3763ad65f52283832ebf058fdf1cslive

06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport Haskell.HatAna as HatAna

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Haskell.HatParser

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slivepickParser :: (Continuity,Bool) -> AParser () (IsaSign.Sign, [Named IsaSign.Sentence])

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slivepickParser c = do

06ba4a61654b3763ad65f52283832ebf058fdf1cslive b <- hatParser

06ba4a61654b3763ad65f52283832ebf058fdf1cslive let res@(Result _ m) = do

06ba4a61654b3763ad65f52283832ebf058fdf1cslive (_, _, sig, sens) <- hatAna (b, HatAna.emptySign, emptyGlobalAnnos)

06ba4a61654b3763ad65f52283832ebf058fdf1cslive transTheory (fst c) (snd c) sig sens

06ba4a61654b3763ad65f52283832ebf058fdf1cslive case m of

06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> fail $ show res

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive Just x -> return x

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slivemain :: IO ()

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slivemain = do

06ba4a61654b3763ad65f52283832ebf058fdf1cslive let err = "command line input error: first argument must be"

06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ " either h (HOL), hc (HOLCF), mh (HOL with theory morphisms),"

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive ++ " mhc (HOLCF with theory morphisms)."

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive l <- getArgs

06ba4a61654b3763ad65f52283832ebf058fdf1cslive case l of

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive [] -> putStrLn err

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive c : fs -> let elm = elem $ map toLower c in

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive mapM_ (process (if elm ["h", "hol"] then (NotCont,False)

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive else if elm ["hc", "holcf"] then (IsCont,False)

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive else if elm ["mh", "mhol"] then (IsCont,True)

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive else if elm ["mhc", "mholcf"] then (IsCont,True)

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive else error err)) fs

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveprocess :: (Continuity,Bool) -> FilePath -> IO ()

06ba4a61654b3763ad65f52283832ebf058fdf1csliveprocess c fn = do

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive putStrLn $ "translating " ++ show fn ++ " to " ++ case c of

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive (IsCont,False) -> "HOLCF"

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive (NotCont,False) -> "HOL"

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive (IsCont,True) -> "HOLCF with theory morphisms"

(NotCont,True) -> "HOL with theory morphisms"

s <- readFile fn

ld <- getEnv "HETS_LIB"

let ds = dropWhile isSpace

s1 = ds s

ns = not . isSpace

(front, rest) = span ns s1

s2 = if front == "module" then dropWhile ns $ ds rest else s1

case runParser (pickParser c) (emptyAnnos ()) fn s2 of

Right (sig, hs) -> do

let tn = takeWhile (/= '.')

(reverse . takeWhile ( \ x -> x /= '/') $ reverse fn) ++ "_"

++ case c of

(IsCont,False) -> "hc"

(NotCont,False) -> "h"

(IsCont,True) -> "mhc"

(NotCont,True) -> "mh"

nsig = sig {theoryName = tn}

doc = printIsaTheory tn ld nsig hs

thyFile = tn ++ ".thy"

putStrLn $ "writing " ++ show thyFile

writeFile thyFile (shows doc "\n")

Left err -> putStrLn $ show err