Implement check of bidirectionalizability.
[darcs-mirror-sem_syn.git] / b18n-combined-cgi.hs
index d69803c..1911a62 100644 (file)
@@ -4,11 +4,18 @@ import Text.XHtml
 import Data.Maybe
 import Data.List
 import Data.ByteString.Lazy.UTF8 (fromString)
+import qualified Data.ByteString.Lazy as BS
 import Control.Monad
 import Control.Applicative ((<$>),(<*>))
 import Text.PrettyPrint.HughesPJ (render)
 import System.IO
+import System.IO.Error hiding ( catch )
 import Text.ParserCombinators.Parsec (ParseError)
+import System.Directory
+import Prelude hiding ( catch )
+import Control.Exception
+import System.Posix.Files ( isDirectory, getSymbolicLinkStatus )
+import System.Posix.Env
 
 
 import Parser
@@ -17,49 +24,72 @@ import Type
 import Shapify
 import AST
 
+import MyInterpret
+import BundledCode
 import JQuery
 
 data PageInfo = PageInfo
-    { scrollX :: Maybe String
+    { config :: Config
+    , scrollX :: Maybe String
     , scrollY :: Maybe String
     , viewFunction :: String
     , parseError :: Maybe String
-    , exMode  :: ExecMode
-    , outMode :: OutputMode
-    , showTypes :: Bool
     , generatedModuleMB :: Maybe String
+    , showCode :: Bool
+    , playCodeMB :: Maybe String
+    , playErrorM :: Maybe String
     } 
 
 page (PageInfo {..}) =
        header << (
-       thetitle << "Combining Syntatic and Semantic Bidirectionalization" +++
+       thetitle << "(Combining) Syntatic and Semantic Bidirectionalization" +++
        style ! [ thetype "text/css" ] << cdata cssStyle +++
        script ! [ thetype "text/javascript", src "?jquery" ] << noHtml +++
         script ! [ thetype "text/javascript" ] << cdata jsCode 
        ) +++
        body ! [ strAttr "onload" "restoreScroll()" ] << (
        thediv ! [theclass "top"] << (
-               thespan ! [theclass "title"] << "Combining Syntatic and Semantic Bidirectionalization" +++
+               thespan ! [theclass "title"] << "(Combining) Syntatic and Semantic Bidirectionalization" +++
                thespan ! [theclass "subtitle"] << "Prototype implementation"
        ) +++
        maindiv << (
-               p << ("This tool allows you to experiment with the "+++
-                      "method described in the paper “" +++
+               p << "This tool allows you to experiment with the bidirectionalization methods described in the following papers: " +++
+                ulist << (
+                    li << (
+                      "“" +++
                      hotlink "http://doi.acm.org/10.1145/1291151.1291162"
                         << "Bidirectionalization transformation based on automatic derivation of view complement functions" +++
-                     "” (ICFP'10) by " +++
+                     "” (ICFP'07) by " +++
                      hotlink "http://www.kb.ecei.tohoku.ac.jp/~kztk/"
-                        << "Kazutaka Matsuda" +++
-                     "."
+                        << "Kazutaka Matsuda" +++ ", " +++
+                      "Zhenjiang Hu, " +++
+                      "Keisuke Nakano, " +++
+                      "Makoto Hamana and " +++
+                      "Masato Takeichi."
+                    ) +++
+                    li << (
+                      "“" +++
+                     hotlink "http://doi.acm.org/10.1145/1480881.1480904"
+                        << "Bidirectionalization for free! (Pearl)" +++
+                     "” (POPL'09) by " +++
+                     hotlink "http://www.iai.uni-bonn.de/~jv/"
+                        << "Janis Voigtländer"
+                    ) +++
+                    li << (
+                      "“" +++
+                     hotlink ""
+                        << "TBT" +++
+                     "” (ICFP'10)"
+                    )
                )
-                       
        ) +++
-        form ! [method "POST",
+        form ! [method "post",
                 action "#",
                 strAttr "onsubmit" "saveScroll()"
             ] << (
                 hidden "scrollx" (fromMaybe "0" scrollX) +++
                 hidden "scrolly" (fromMaybe "0" scrollY) +++
+                hidden "showCode" (show showCode) +++
                maindiv << (
                         p << (
                                "Please enter the view function. (TODO: Elaborate this text)"
@@ -67,7 +97,7 @@ page (PageInfo {..}) =
 
                        p << (
                                concatHtml (map (\(name,thisCode) -> 
-                                       radio "load" name
+                                       radio "loadCode" name
                                        ! (if thisCode == viewFunction then [checked] else [])
                                        +++ name +++ " "
                                ) examples) +++
@@ -87,43 +117,60 @@ page (PageInfo {..}) =
                maindiv ! [ identifier "output" ]<< (
                        p << (
                                "You can calculate a derived put function with various options:" ) +++
-                       p << ( "Execution mode: " +++
-                              concatHtml (map (\mode -> 
-                                 radio "execMode" (show mode) 
-                                       ! (guard (mode == exMode) >> return checked)
-                                       +++ show mode +++ " "
-                                ) [Normal, Shapify, ShapifyPlus]) +++ br +++
-                              "Output mode: " +++
+                       p << ( "Output mode: " +++
                               concatHtml (map (\mode -> 
-                                 radio "outputMode" (show mode) 
-                                       ! (guard (mode == outMode) >> return checked)
+                                 radio "b18nMode" (show mode) 
+                                       ! (guard (mode == b18nMode config) >> return checked)
                                        +++ show mode +++ " "
-                                ) [PseudoCode, HaskellCode, ForwardCode]) +++ br +++
-                              "Show types " +++ checkbox "showTypes" "showTypes"
-                                        ! (guard showTypes >> return checked)
-                                        +++ br +++
+                                ) [SyntacticB18n, SemanticB18n, CombinedB18n]) +++ br +++
                               mkSubmit True BiDi
                        ) +++
                         ( htmlMB generatedModuleMB $ \ generatedModule -> 
                             {- maybe noHtml outputErrors errors +++ -}
-                            p << ("Result:"+++ br +++
-                                textarea ! [name "gencode", cols "120"
-                                           , rows (show (1 + length (lines generatedModule)))
-                                           ] << generatedModule
+                            p << ("Result Code" +++
+                                thespan ! [ identifier "hideShow"
+                                          , thestyle "display:none"] << (
+                                    " (" +++ hotlink "javascript:" << "Hide/Show" +++ ")"
+                                ) +++ ":" +++ br +++
+                                pre ! [identifier "genCode" ] << generatedModule
 
                             )
+
                         )
-               )
+               ) +++
+                ( htmlMB playCodeMB $ \playCode -> maindiv << ( 
+                    p << (  "You can now play with the code. You can modify the " +++
+                            tt << "source" +++ " and calculate the " +++
+                            tt << "view" +++ ", or modify the " +++
+                            tt << "view" +++ " and calculate an updated "+++
+                            tt << "source" +++ "." +++ br +++
+                            textarea ! [name "playCode", cols "120", rows "8" ] << playCode
+                    ) +++
+                    p << ( "Evaluate " +++
+                           mkSubmit True EvalGet +++ " " +++
+                           mkSubmit True EvalPut
+                    )
+                )) +++
+                ( htmlMB playErrorM $ \playError -> maindiv << ( 
+                    p << (
+                        strong << "An error occurred while evaluating your code:" +++ br +++
+                        pre << playError
+                        )
+                ))
        ) +++
         maindiv << (
-               p << (
+           p << (
                "The source code of this application and the underlying library can be found " +++
                hotlink "TODO" << "here"+++
-               ".") +++
-               p << ("© 2010 Joachim Breitner <" +++
-                      hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
-                     ">")
-               )       
+               ". " +++
+                "The code for the web interface is based on " +++
+                hotlink "http://www-ps.iai.uni-bonn.de/cgi-bin/bff.cgi" << 
+                    "the demo interface from “Bidirectionalization for free!”"
+            ) +++
+           p << ("© 2010 Joachim Breitner <" +++
+                hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
+             ">")
+           )   
        )
        
 
@@ -133,30 +180,30 @@ maindiv = thediv ! [theclass "main"]
         
 examples =
        [ ("init", unlines
-               [ "init (Nil)         = Nil"
-               , "init (Cons(a,Nil)) = Nil"
-               , "init (Cons(a,Cons(b,x))) = Cons(a,initWork(b,x))"
-               , "initWork(a,Nil)       = Nil"
-               , "initWork(a,Cons(b,x)) = Cons(a,initWork(b,x))"
+               [ "init []      = []"
+               , "init [a]     = []"
+               , "init (a:b:x) = a:initWork b x"
+               , "initWork a []    = []"
+               , "initWork a (b:x) = a:initWork b x"
                ])
        , ("initHalf", unlines
-               [ "initHalf(Nil)       = Nil"
-               , "initHalf(Cons(a,x)) = Cons(a,initHalfWork(x,x))"
+               [ "initHalf []    = []"
+               , "initHalf (a:x) = a:initHalfWork x x"
                , ""
-               , "initHalfWork(xs, Nil)         = Nil"
-               , "initHalfWork(xs, Cons(x,Nil)) = Nil"
-               , "initHalfWork(Cons(a,x), Cons(b,Cons(c,y)))"
-               , "                    = Cons(a,initHalfWork(x,y))"
+               , "initHalfWork xs  []  = []"
+               , "initHalfWork xs  [x] = []"
+               , "initHalfWork (a:x) (b:c:y)"
+               , "                    = a:initHalfWork x y"
                ])
-       , ("seive", unlines
-               [ "seive (Nil)               = Nil"
-               , "seive (Cons(a,Nil))       = Nil"
-               , "seive (Cons(a,Cons(b,x))) = Cons(b,seive(x))"
+       , ("sieve", unlines
+               [ "sieve []      = []"
+               , "sieve [a]     = []"
+               , "sieve (a:b:x) = b:sieve x"
                ])
        , ("rev", unlines
-               [ "reverse(xs) = rev(xs,Nil)"
-               , "rev(Nil,y)       = y"
-               , "rev(Cons(a,x),y) = rev(x,Cons(a,y))"
+               [ "reverse xs = rev xs []"
+               , "rev []    y = y"
+               , "rev (a:x) y = rev x (a:y)"
                ])
        ]
 
@@ -172,22 +219,25 @@ outputErrors s =
 mkSubmit active what = submit (submitId what) (submitLabel what)
                       ! if active then [] else [disabled]
 
-data Run = Get | Check | Load | BiDi
+data Run = Get | Check | Load | BiDi | EvalPut | EvalGet
 
 
 submitId Get = "get source"
 submitId Check = "check"
 submitId Load = "load"
 submitId BiDi = "submitBiDi"
+submitId EvalPut = "evalPut"
+submitId EvalGet = "evalGet"
 
 submitCode Get   = Just ("get source")
 submitCode Check = Nothing
 submitCode Load  = Nothing
-submitCode BiDi = Just ("bidirectionalize")
 
-submitLabel Check = "Re-Parse definition"
-submitLabel Load  = "Load example"
-submitLabel x   = fromJust (submitCode x)
+submitLabel Check =   "Re-Parse definition"
+submitLabel Load  =   "Load example"
+submitLabel EvalGet = "view = get source"
+submitLabel EvalPut = "result = put source view"
+submitLabel BiDi =    "bidirectionalize"
 
 main = runCGI (handleErrors cgiMain)
 
@@ -226,42 +276,121 @@ jQueryMain = do
         setHeader "Cache-control" "max-age=36000000" -- 1000 h
         outputFPS $ jQueryCode
     
+defaultPlayCode (Config{..}) get =
+        Just $ unlines
+            [ "get s = Main." ++ get ++ " s"
+            , "put s v = " ++ put
+            , ""
+            , "source = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]"
+            ]
+    where put | b18nMode == SyntacticB18n =
+                    get ++ "_140_B s v"
+              | b18nMode == SemanticB18n =
+                    get ++ "_B s v"
+              | b18nMode == CombinedB18n =
+                    "fromMaybe (error \"Could not handle shape change.\") $ " ++
+                    get ++ "_Bbd rear 42 s v"
 
 formMain = do
         setHeader "Content-type" "application/xhtml+xml; charset=UTF-8"
 
-        exMode  <- maybe Normal read <$> getInput "execMode"
-        outMode <- maybe PseudoCode read <$> getInput "outputMode"
-        showTypes <- isJust <$> getInput "showTypes"
+        conf <- do
+            b18nMode' <- maybe CombinedB18n read <$> getInput "b18nMode"
+            return $ defaultConfig
+                { isHaskellify = True
+                , b18nMode = b18nMode'
+                , execMode = ShapifyPlus
+                }
        
        todo <- msum <$> sequence (
             map (\what -> fmap (const what) <$> getInput (submitId what))
-            [ BiDi, Get, Check, Load ])
+            [ BiDi, Get, Check, Load, EvalPut, EvalGet])
         
-       code <- fromMaybe defaultCode <$> getInput "code"
-       
+       code <- filter (/= '\r') <$> fromMaybe defaultCode <$> getInput "code"
+
         code <- case todo of
-            Just Load -> do loadWhat <- getInput "load"
+            Just Load -> do loadWhat <- getInput "loadCode"
                             return $ fromMaybe code $ loadWhat >>= flip lookup examples 
             _ -> return code
         
-        let mbAST = parseString code
+        let eAST = parseString code
+
+
+        let parseError = either (Just . show) (const Nothing) eAST
 
-        let conf = defaultConfig { outputMode = outMode, execMode = exMode, isShowType = showTypes }
-        let parseError = either (Just . show) (const Nothing) mbAST
+        let (genCodeM,getM) = case (todo,eAST) of
+                (Just Load, _) -> (Nothing, Nothing)
+                (Just _, Right ast) ->
+                    (  Just $ render $
+                       outputCode conf True  ast (introNat $ shapify $ typeInference ast)
+                    ,  firstDeclaredName ast
+                    )
+                _ -> (Nothing, Nothing)
 
-        let genCode = case (todo,mbAST) of
-                (Just Load, _) -> Nothing
-                (Just _, Right ast) -> Just $ render $ case exMode of 
-                       Normal -> outputCode conf False ast (typeInference ast)
-                       Shapify -> outputCode conf False ast (shapify $ typeInference ast)
-                       ShapifyPlus -> outputCode conf True  ast (introNat $ shapify $ typeInference ast)
-                _ -> Nothing
+        showCode <- maybe False read <$> getInput "showCode"
+
+        pcM <- getInput "playCode" 
+        -- Playcode can only by used when the output is exMode
+        (playCode, playErrorM) <- -- if outMode /= HaskellCode then return (Nothing, Nothing) else
+            case (todo,getM,genCodeM,pcM) of
+            -- The user successfully generated code to play with, insert default playCode.
+            -- Do not use the user input, as he probably switched to a new example.
+            (Just BiDi, Just get, Just _, _) ->
+                return (defaultPlayCode conf get, Nothing)
+            -- The user played with the code
+            (Just EvalGet, Just get, Just genCode, Just pc) -> do
+                view <- liftIO $ evaluateWith genCode pc ("get source")
+                case view of 
+                    Left err -> return $ (Just pc, Just err)
+                    Right dat -> return $ (\r -> (Just r, Nothing))
+                                        $ addDefiniton "view" dat 
+                                        $ delDefinition "result"
+                                        $ pc
+            (Just EvalGet, Just get, Just genCode, Nothing) -> do
+                return (defaultPlayCode conf get, Nothing)
+            (Just EvalPut, Just get, Just genCode, Just pc) -> do
+                view <- liftIO $ evaluateWith genCode pc ("put source view")
+                case view of 
+                    Left err -> return $ (Just pc, Just err)
+                    Right dat -> return $ (\r -> (Just r, Nothing))
+                                        $ addDefiniton "result" dat 
+                                        $ pc
+            (Just EvalPut, Just get, Just _, Nothing) -> do
+                return (defaultPlayCode conf get, Nothing)
+            _ -> return (Nothing, Nothing)
 
         scrollX <- getInput "scrollx"
         scrollY <- getInput "scrolly"
 
-        outputFPS $ fromString $ showHtml $ page (PageInfo scrollX scrollY code parseError exMode outMode showTypes genCode)
+        outputFPS $ fromString $ showHtml $ page $
+            PageInfo conf
+                     scrollX
+                     scrollY
+                     code
+                     parseError
+                     genCodeM
+                     showCode
+                     playCode
+                     playErrorM
+
+evaluateWith :: String -> String -> String -> IO (Either String String)
+evaluateWith genCode playCode expr =
+    withinTmpDir $ do
+        BS.writeFile "BUtil.hs" bUtilCode
+        writeFile "Main.hs" $ "module Main where\n" ++ genCode
+        liftIO $ catchInterpreterErrors $ simpleInterpret mods imports playCode expr
+  where mods = 
+            [ "BUtil"
+            , "Main"
+            --, "Data.Maybe"
+            ]
+        imports = mods ++
+            [ "Data.Maybe"
+            , "Prelude"
+            ]
+
+withFullSource genCode playCode = genCode' ++ "\n" ++ playCode
+    where genCode' = unlines . filter (not . isPrefixOf "import") . lines $ genCode
 
 astInfo (Left err) = maindiv << p << (
        "Can not parse your definition:" +++ br +++
@@ -269,25 +398,7 @@ astInfo (Left err) = maindiv << p << (
        mkSubmit True Check)
 
 astInfo (Right source) = maindiv << (
-       p << ("Definition parsed succesfully"
-{-             "Your definitions have the following types: " +++
-               pre << ("get :: " ++ getType ++ "\n"++
-                       "source :: " ++ sourceType) +++
-               "Therefore, an updater can be derived by " +++
-               case (canBff, canBffEq, canBffOrd) of
-                       (True, _, _) -> 
-                               tt << "bff" +++ ", " +++
-                               tt << "bff_Eq" +++ ", and " +++
-                               tt << "bff_Ord" +++ "."
-                       (False, True, _) -> 
-                               tt << "bff_Eq" +++ " and " +++
-                               tt << "bff_Ord" +++ "."
-                       (False, False, True) -> 
-                               tt << "bff_Ord" +++ " only."
-                       (False, False, False) -> 
-                               "none of the " +++ tt << "bff" +++ " functions."
--}                                
-       ) +++
+       p << ("Definition parsed succesfully") +++
        p << mkSubmit True Check
        )
 
@@ -313,12 +424,80 @@ cssStyle = unlines
 
 jsCode = unlines 
     [ "function saveScroll () {"
-    , "    $(\"#scrolly\").val($(\"html\").scrollTop());"
+    , "    $('#scrolly').val($('html').scrollTop());"
     , "}"
     , "function restoreScroll () {"
-    , "    $(\"html\").scrollTop($(\"#scrolly\").val());"
+    , "    $('html').scrollTop($('#scrolly').val());"
     , "}"
+    , "$(document).ready(function () {"
+    , "   $('#hideShow').show();"
+    , "   if ($('#showCode').val() == 'False')"
+    , "     { $('#genCode').hide(); };"
+    , "   $('#hideShow a').click(function () {"
+    , "      $('#showCode').val("
+    , "         $('#genCode').is(':visible') ? 'False' : 'True'"
+    , "      );"
+    , "      $('#genCode').toggle('slow');"
+    , "   })"
+    , "})"
     ]
 
 htmlMB Nothing  f = noHtml
 htmlMB (Just x) f = f x
+
+readOnly = emptyAttr "readonly"
+
+
+firstDeclaredName (AST []) = Nothing
+firstDeclaredName (AST (Decl n _ _ _:_)) = Just (show n)
+
+{-
+ - Temp-Dir functions taken from XMonad/Lock.hs and simplified.
+ - It also changes TMP so that hint’s temporary files are stored within this directory
+ -}
+withinTmpDir :: IO a -> IO a
+withinTmpDir job = do
+  absolute_name <- (++ "/sem_syn.cgi") <$> getTemporaryDirectory
+  formerdir <- getCurrentDirectory
+  formerTMP <- getEnv "TMPDIR"
+  bracket (do dir <- create_directory absolute_name 0
+              setEnv "TMPDIR" dir True  
+              return dir
+          )
+          (\dir -> do setCurrentDirectory formerdir
+                      maybe (unsetEnv "TMPDIR") (\p -> setEnv "TMPDIR" p True) formerTMP
+                      rmRecursive dir)
+          (const job)
+    where newname name 0 = name
+          newname name n = name ++ "-" ++ show n
+          create_directory :: FilePath -> Int -> IO FilePath
+          create_directory name n
+              = do createDirectory $ newname name n
+                   setCurrentDirectory $ newname name n
+                   getCurrentDirectory
+                `catch` (\e -> if isAlreadyExistsError e
+                               then create_directory name (n+1)
+                               else throwIO e)
+
+rmRecursive :: FilePath -> IO ()
+rmRecursive d =
+    do isd <- isDirectory <$> getSymbolicLinkStatus d
+       if not isd
+          then removeFile d
+          else when isd $ do conts <- actual_dir_contents
+                             withCurrentDirectory d $
+                               mapM_ rmRecursive conts
+                             removeDirectory d
+    where actual_dir_contents = -- doesn't include . or ..
+              do c <- getDirectoryContents d
+                 return $ filter (/=".") $ filter (/="..") c
+
+withCurrentDirectory :: FilePath -> IO r -> IO r
+withCurrentDirectory name m =
+    bracket
+        (do cwd <- getCurrentDirectory
+            when (name /= "") (setCurrentDirectory name)
+            return cwd)
+        (\oldwd -> setCurrentDirectory oldwd)
+        (const m)
+