{-# LANGUAGE OverloadedStrings, TemplateHaskell #-} module Main where import Prelude import Control.Monad (unless) import Control.Monad.IO.Class (liftIO) import Control.Arrow import Control.DeepSeq (force) import Control.Exception (evaluate, catch, SomeException) import Data.FileEmbed import Data.List (intercalate) import Data.Maybe (fromMaybe) import Data.Version (showVersion) import Paths_smcdel (version) import Web.Scotty import qualified Data.Text as T import qualified Data.Text.Encoding as E import qualified Data.Text.Lazy as TL import Data.HasCacBDD.Visuals (svgGraph) import qualified Language.Javascript.JQuery as JQuery import Language.Haskell.TH.Syntax import Network.Wai.Handler.Warp (defaultSettings, setHost, setPort) import System.Environment (lookupEnv) import Text.Read (readMaybe) import SMCDEL.Internal.Lex import SMCDEL.Internal.Parse import SMCDEL.Internal.Sanity import SMCDEL.Symbolic.S5 import SMCDEL.Internal.TexDisplay import SMCDEL.Translations.S5 import SMCDEL.Language main :: IO () main = do putStrLn $ "SMCDEL " ++ showVersion version ++ " -- https://github.com/jrclogic/SMCDEL" port <- fromMaybe 3000 . (readMaybe =<<) <$> lookupEnv "PORT" putStrLn $ "Please open this link: http://127.0.0.1:" ++ show port ++ "/index.html" let mySettings = Options 1 (setHost "127.0.0.1" $ setPort port defaultSettings) scottyOpts mySettings $ do get "" $ redirect "index.html" get "/" $ redirect "index.html" get "/index.html" . html . TL.fromStrict $ addVersionNumber $ embeddedFile "index.html" get "/jquery.js" . html . TL.fromStrict $ embeddedFile "jquery.js" get "/ace.js" . html . TL.fromStrict $ embeddedFile "ace.js" get "/viz-lite.js" . html . TL.fromStrict $ embeddedFile "viz-lite.js" get "/getExample" $ do this <- param "filename" html . TL.fromStrict $ embeddedFile this post "/check" $ do smcinput <- param "smcinput" case alexScanTokensSafe smcinput of Left pos -> webError Lex (Just pos) [] Right lexResult -> case parse lexResult of Left pos -> webError Parse (Just pos) [] Right ci@(CheckInput vocabInts lawform obs jobs) -> case sanityCheck ci of msgs@(_:_) -> do webError Sanity Nothing msgs [] -> do let mykns = KnS (map P vocabInts) (boolBddOf lawform) (map (second (map P)) obs) knstring <- liftIO $ showStructure mykns results <- liftIO $ doJobsWebSafe mykns jobs html $ mconcat [ TL.pack knstring , "
" ++ result ++ "
\n" ++ rest doJobWeb :: KnowStruct -> Job -> String doJobWeb mykns (TrueQ s f) = unlines [ "\\( (\\mathcal{F}, " ++ sStr ++ " ) " , if evalViaBdd (mykns, map P s) f then "\\vDash" else "\\not\\vDash" , (texForm . simplify) f , "\\)" ] where sStr = " \\{ " ++ intercalate "," (map (\i -> "p_{" ++ show i ++ "}") s) ++ " \\}" doJobWeb mykns (ValidQ f) = unlines [ "\\( \\mathcal{F} " , if validViaBdd mykns f then "\\vDash" else "\\not\\vDash" , (texForm . simplify) f , "\\)" ] doJobWeb mykns (WhereQ f) = unlines [ "At which states is \\(" , (texForm . simplify) f , "\\) true?", show kind, " error"
, if not (null msgs) then ": " ++ intercalate "
" msgs else ""
, case mpos of
Just (lin,col) -> concat
[ " in line ", show lin, ", column ", show col, "