module Agda.Compiler.Alonzo.Haskell where import Language.Haskell.Syntax import Language.Haskell.Pretty import System.IO dummyLoc :: SrcLoc dummyLoc = SrcLoc "=alonzo=" 0 0 hsModule :: String -> [HsDecl] -> HsModule hsModule name decls = HsModule dummyLoc (Module name) Nothing [] decls hsModuleImporting :: String -> [String] -> [String] -> [HsDecl] -> HsModule hsModuleImporting name imps qimps decls = HsModule dummyLoc (Module name) Nothing (map hsImport imps ++ impRTS : impRTP : map hsQImport qimps) decls hsImport :: String -> HsImportDecl hsImport s = HsImportDecl dummyLoc (Module s) False Nothing Nothing hsQImport :: String -> HsImportDecl hsQImport s = HsImportDecl dummyLoc (Module s) True Nothing Nothing impRTS :: HsImportDecl impRTS = hsImport "RTS" impRTP :: HsImportDecl impRTP = hsQImport "RTP" hsUndefined :: HsExp hsUndefined = hsVar "undefined" hsError :: String -> HsExp hsError s = HsApp (hsVar "error") (HsLit $ HsString s) hsCast e@(HsVar _) = HsApp (hsVar "cast") e hsCast e@(HsCon _) = HsApp (hsVar "cast") e hsCast e = HsApp (hsVar "cast") (HsParen e) hsVar :: String -> HsExp hsVar s = HsVar $ UnQual $ HsIdent s hsCon :: String -> HsExp hsCon s = HsCon $ UnQual $ HsIdent s hsLam :: String -> HsExp -> HsExp hsLam n e = HsLambda dummyLoc [HsPVar (HsIdent n)] e hsAp :: HsExp -> HsExp -> HsExp hsAp e1 e2 = HsApp (hsCast e1) $ HsParen (hsCast e2) outputHsModule s hsmod numOfMainS = do handle <- openFile (s++".hs") WriteMode printHsModule handle hsmod case numOfMainS of Nothing -> return () Just i -> printHsMain handle i hClose handle printHsMain handle i = do hPutStrLn handle mainStr where -- mainStr = "main = putStrLn d" ++ (show i) mainStr = "main = d" ++ show i printHsModule :: Handle -> HsModule -> IO () printHsModule handle hsmod = do hPutStrLn handle "{-# OPTIONS -fglasgow-exts #-}" hPutStrLn handle "" hPutStrLn handle "-- Generated by Alonzo" hPutStrLn handle "" hPutStrLn handle $ prettyPrint $ hsmod printHsDecls :: [HsDecl] -> IO () printHsDecls ds = mapM_ (putStrLn . prettyPrint) ds data AlDecl = AlDecl [HsDecl] | AlComment String printAlDecl :: AlDecl -> IO() printAlDecl (AlDecl ds) = printHsDecls ds printAlDecl (AlComment s) = putStrLn $ "{- "++s++" -}" printAlModule :: String -> [AlDecl] -> IO() printAlModule name ds = do putStrLn "{-# OPTIONS -fglasgow-exts -cpp #-}" putStrLn "" putStrLn "-- Generated by Alonzo" putStrLn "" putStrLn $ "module " ++ name ++ " where" putStrLn "import RTS" mapM_ printAlDecl ds {- type sigs HsExp = ... HsExpTypeSig SrcLoc HsExp HsQualType data HsQualType = HsQualType HsContext HsType type HsContext = [HsAsst] HsType = ... HsTyCon HsQName -} hsTypedExp :: HsQName -> HsExp -> HsExp hsTypedExp qn e = HsExpTypeSig dummyLoc e $ HsQualType [] $ HsTyCon qn hsPreludeName :: String -> HsQName hsPreludeName s = Qual prelude_mod $ HsIdent s hsPreludeTypedExp :: String -> HsExp -> HsExp hsPreludeTypedExp s e = hsTypedExp (hsPreludeName s) e