gulcii-0.3: src/Main.hs
{-
gulcii -- graphical untyped lambda calculus interpreter
Copyright (C) 2011, 2013, 2017 Claude Heiland-Allen
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License along
with this program; if not, write to the Free Software Foundation, Inc.,
51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
-}
module Main (main) where
import Control.Applicative ((<$>))
import Control.Concurrent (forkIO, killThread, threadDelay, newChan, readChan, writeChan)
import Control.Monad (forever, when, unless, forM_)
import qualified Data.Map.Strict as M
import Data.Maybe (isJust)
import Data.IORef (IORef, newIORef, readIORef, writeIORef, atomicModifyIORef)
import System.IO (hSetBuffering, BufferMode(LineBuffering), stdout)
import System.IO.Error (catchIOError)
import System.FilePath ((</>), (<.>))
import Graphics.UI.Gtk hiding (Meta, Settings)
import Graphics.Rendering.Cairo hiding (width, height)
import Paths_gulcii (getDataFileName)
import qualified Command as C
import qualified Meta as M
import Setting (Settings)
import qualified Setting
import qualified Sugar as S
import qualified Bruijn as B
import qualified Graph as G
import qualified GC as GC
import qualified Reduce as R
import qualified Layout as L
import qualified Draw as D
import qualified Parse as P
data Interpret = Fail | Skip | Define String G.Term | Pure G.Term | Meta M.Meta
deriving (Read, Show, Eq, Ord)
interpret :: String -> Interpret
interpret l =
case P.unP C.parse `fmap` P.tokenize (P.decomment l) of
Just ((C.Define d sterm, []):_) ->
case S.desugar sterm of
Just term -> Define d . G.graph . B.bruijn $ term
_ -> Fail
Just ((C.Evaluate sterm, []):_) ->
case S.desugar sterm of
Just term -> Pure . G.graph . B.bruijn $ term
_ -> Fail
Just ((C.Meta m, []):_) -> Meta m
Just [] -> Skip
_ -> Fail
main :: IO ()
main = do
args <- initGUI
let (width, height, fullscreen) = case args of
[w,h,"fullscreen"] -> (read w, read h, True)
[w,h] -> (read w, read h, False)
_ -> (1280, 720, False)
envR <- newIORef M.empty
lRef <- newIORef Nothing
evalR <- newIORef Nothing
settingsR <- newIORef Setting.defaults
outC <- newChan
let out = writeChan outC
win <- windowNew
_ <- onDestroy win mainQuit
windowSetDefaultSize win width height
when fullscreen $ do
windowSetGeometryHints win (Nothing `asTypeOf` Just win)
(Just (width, height)) (Just (width, height)) Nothing Nothing Nothing
set win [ windowDecorated := False ]
windowSetKeepAbove win True
windowMove win 0 0
vb <- vBoxNew False 0
hb <- hPanedNew
tt <- textTagTableNew
tagInputRem <- textTagNew Nothing
tagInputDef <- textTagNew Nothing
tagInputPure <- textTagNew Nothing
tagInputRun <- textTagNew Nothing
tagInputMeta <- textTagNew Nothing
tagOutput <- textTagNew Nothing
tagOutputMeta <- textTagNew Nothing
tagError <- textTagNew Nothing
set tagInputRem [ textTagForeground := "cyan" ]
set tagInputDef [ textTagForeground := "green" ]
set tagInputPure [ textTagForeground := "yellow" ]
set tagInputRun [ textTagForeground := "orange" ]
set tagInputMeta [ textTagForeground := "blue" ]
set tagOutput [ textTagForeground := "magenta" ]
set tagOutputMeta [ textTagForeground := "pink" ]
set tagError [ textTagForeground := "red" ]
textTagTableAdd tt tagInputRem
textTagTableAdd tt tagInputDef
textTagTableAdd tt tagInputPure
textTagTableAdd tt tagInputRun
textTagTableAdd tt tagInputMeta
textTagTableAdd tt tagOutput
textTagTableAdd tt tagOutputMeta
textTagTableAdd tt tagError
tf <- textBufferNew (Just tt)
tb <- textBufferNew (Just tt)
tv <- textViewNewWithBuffer tf
mk <- textMarkNew Nothing False
it <- textBufferGetIterAtOffset tf (-1)
textBufferAddMark tf mk it
textViewSetEditable tv False
textViewSetWrapMode tv WrapWord
da <- drawingAreaNew
_ <- da `on` exposeEvent $ do
dw <- eventWindow
liftIO $ do
ml <- atomicModifyIORef lRef (\m -> (Nothing, m))
case ml of
Nothing -> return ()
Just l -> do
(ww, hh) <- drawableGetSize dw
renderWithDrawable dw $ do
D.draw (fromIntegral ww) (fromIntegral hh) l
return True
en <- entryNew
entrySetWidthChars en 25
font <- fontDescriptionFromString "Monospaced 18"
widgetModifyFont tv (Just font)
widgetModifyFont en (Just font)
sw <- scrolledWindowNew Nothing Nothing
scrolledWindowSetPolicy sw PolicyAutomatic PolicyAlways
containerAdd sw tv
al <- alignmentNew 1 0 1 1
set al [ containerChild := da ]
if Setting.newsOnTop Setting.defaults
then do
boxPackStart vb en PackNatural 0
boxPackStart vb sw PackGrow 0
else do
boxPackStart vb sw PackGrow 0
boxPackStart vb en PackNatural 0
panedPack1 hb vb False True
panedPack2 hb al True True
set win [ containerChild := hb ]
containerSetFocusChain vb [toWidget en]
let scrollDown = do
textViewScrollToMark tv mk 0 Nothing
addText tag txt = do
newsOnTop <- Setting.newsOnTop <$> readIORef settingsR
start' <- textBufferGetIterAtOffset tb 0
end' <- textBufferGetIterAtOffset tb (-1)
textBufferDelete tb start' end'
textBufferInsert tb start' (unlines [txt])
start <- textBufferGetIterAtOffset tb 0
end <- textBufferGetIterAtOffset tb (-1)
textBufferApplyTag tb tag start end
pos <- textBufferGetIterAtOffset tf (if newsOnTop then 0 else -1)
textBufferInsertRange tf pos start end
pos' <- textBufferGetIterAtOffset tf (if newsOnTop then 0 else -1)
textBufferMoveMark tf mk pos'
_ <- en `onEntryActivate` do
let exec echo txt =
case interpret txt of
Fail -> addText tagError txt
Skip -> when echo $ do
addText tagInputRem txt
entrySetText en ""
Define def term -> do
when echo $ do
addText tagInputDef txt
entrySetText en ""
atomicModifyIORef envR (\defs -> (M.insert def term defs, ()))
Pure term -> do
when echo $ do
addText tagInputPure txt
entrySetText en ""
mtid <- readIORef evalR
case mtid of
Nothing -> return ()
Just tid -> killThread tid
tid <- forkIO $ evaluator "gulcii-" 0 settingsR 500000 lRef out envR M.empty term goPure
writeIORef evalR (Just tid)
Meta M.Start -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
_ <- forkIO $ do
out "start;"
return ()
Meta M.Stop -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
_ <- forkIO $ do
out "stop;"
return ()
Meta M.Quit -> do
_ <- forkIO $ do
out "quit;"
postGUISync mainQuit
return ()
Meta M.Clear -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
atomicModifyIORef envR (\_ -> (M.empty, ()))
Meta M.Browse -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
defs <- readIORef envR
addText tagOutputMeta(unwords (M.keys defs))
Meta (M.Load f) -> do
when echo $ do
addText tagInputMeta txt
f' <- getDataFileName ("lib" </> f <.> "gu")
s <- (fmap Right (readFile f')) `catchIOError` (return . Left . show)
case s of
Right t -> do
when echo $ do
entrySetText en ""
mapM_ (exec False) (lines t)
Left e ->
addText tagError e
Meta (M.Get s) -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
Meta (M.Set s) -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
atomicModifyIORef settingsR $ (\ss -> (Setting.set s True ss, ()))
addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
Meta (M.UnSet s) -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
atomicModifyIORef settingsR $ (\ss -> (Setting.set s False ss, ()))
addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
Meta (M.Toggle s) -> do
when echo $ do
addText tagInputMeta txt
entrySetText en ""
atomicModifyIORef settingsR $ (\ss -> (Setting.set s (not (Setting.get s ss)) ss, ()))
addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
txt <- entryGetText en
exec True txt
scrollDown
_ <- forkIO $ do
hSetBuffering stdout LineBuffering
forever $ do
settings <- readIORef settingsR
s <- readChan outC
when (Setting.echoToStdOut settings) $ putStrLn s
when (Setting.echoToGUI settings) $ postGUIAsync (addText tagOutput s >> scrollDown)
_ <- flip timeoutAdd 10 $ do
ml <- atomicModifyIORef lRef (\m -> (m, m))
when (isJust ml) $ widgetQueueDraw da
return True
widgetShowAll win
mainGUI
type Go = G.References -> G.Term -> IO (G.Term, G.References)
goPure :: Go
goPure refs term = return (term, refs)
evaluator :: String -> Int -> IORef Settings -> Int -> IORef (Maybe L.Layout) -> (String -> IO ()) -> IORef G.Definitions -> G.References -> G.Term -> Go -> IO ()
evaluator pngPrefix frame settingsR tick layout out defsR refs term go = do
defs <- readIORef defsR
settings <- readIORef settingsR
when (Setting.traceEvaluation settings) $ do
out $ " " ++ G.pretty term
unless (M.null refs) $ do
out " where"
forM_ (M.toList refs) $ \(r, t) -> do
out $ " #" ++ show r ++ " = " ++ G.pretty t
let (refs1, term1)
| Setting.collectGarbage settings = GC.gc refs term
| otherwise = (refs, term)
collectedGarbage = term1 /= term || refs1 /= refs
when (Setting.traceEvaluation settings && collectedGarbage) $ do
out "$\\to$ {- collect garbage -}"
out $ " " ++ G.pretty term1
unless (M.null refs1) $ do
out " where"
forM_ (M.toList refs1) $ \(r, t) -> do
out $ " #" ++ show r ++ " = " ++ G.pretty t
(term0, refs0) <- go refs1 term1
(l, L.Counts c1 c2 c3 c4 c5 c6 c7) <- atomicModifyIORef layout $ \_ ->
let l@(L.Layout lt _ _ _) = L.layout term0 refs0
in (Just l, (l, L.counts lt))
when (Setting.saveImages settings) $ do
withImageSurface FormatRGB24 1920 1080 $ \surface -> do
renderWith surface $ do
let g = 23 / 255
setSourceRGB g g g
paint
D.draw 1920 1080 l
surfaceWriteToPNG surface (pngPrefix ++ show frame ++ ".png")
when (Setting.emitStatistics settings) $ do
out $ "statistics " ++ unwords (map show [c1,c2,c3,c4,c5,c6,c7]) ++ ";"
when (Setting.realTimeDelay settings) $ do
threadDelay tick
let tick'
| Setting.realTimeAcceleration settings = ceiling (fromIntegral tick * 0.97 + 0.03 * 42000 :: Double)
| otherwise = tick
case R.reduce defs refs0 term0 of
Nothing -> do
when (Setting.traceEvaluation settings) $ do
out "$\\to$ {- in normal form -}"
out " $\\qedsymbol$"
when (Setting.retryIrreducible settings) $ do
evaluator pngPrefix (frame + 1) settingsR tick layout out defsR refs0 term0 go
Just (reason, (refs', term')) -> do
when (Setting.traceEvaluation settings) $ do
out $ "$\\to$ {- " ++ (case reason of
R.Beta -> "beta reduce"
R.RefInst -> "instantiate reference"
R.Rebound var -> "definition of \"" ++ var ++ "\""
R.Extrude -> "scope extrude"
) ++ " -}"
evaluator pngPrefix (frame + 1) settingsR tick' layout out defsR refs' term' go