diff --git a/Main.hs b/Main.hs index 8ebc37b..ed3f1df 100644 --- a/Main.hs +++ b/Main.hs @@ -4,15 +4,12 @@ module Main where import Prelude hiding (FilePath) import Data.String (fromString) import Data.Maybe (fromMaybe) -import Parse -import Text.Parsec.String import Compile import Control.Arrow import Control.Monad import Control.Monad.Except import Control.Monad.Catch import Control.Concurrent (threadDelay) -import qualified Data.Text as T import qualified Data.Text.IO as T import Options.Applicative hiding (Parser) import Text.LaTeX.Base.Parser @@ -30,8 +27,6 @@ data AppData = AppData , watch :: Bool } -data Format = Proof | Tex deriving (Show) - opts :: ParserInfo AppData opts = info (helper <*> optParser) ( fullDesc @@ -50,18 +45,9 @@ opts = info (helper <*> optParser) path :: Monad m => String -> m FilePath path = liftM fromString . str -fileFormat :: Monad m => FilePath -> Err m Format -fileFormat s = case fromMaybe "no extension" (extension s) of - "proof" -> return Proof - "tex" -> return Tex - e -> throwError (T.unpack e) - outputPath :: FilePath -> FilePath outputPath p = replaceExtension p "html" -proofReader :: MonadIO m => FilePath -> Err m RawDocument -proofReader = ExceptT . liftIO . fmap (left show) . parseFromFile document . encodeString - texReader :: (MonadIO m, Functor m) => FilePath -> Err m RawDocument texReader = (ExceptT . liftIO . fmap (left show) . parseLaTeXFile . encodeString) >=> decorate >=> translate @@ -96,37 +82,27 @@ loadResources = readDataFile = (`catch` (\(_::IOError) ->throwError "Could not read data files")) . liftIO . (T.readFile <=< getDataFileName) +pkgPath :: FilePath -> FilePath -> FilePath pkgPath inputPath outputDir = outputDir addExtension (basename inputPath) "proofpkg" compileAndOutput :: (MonadIO m, MonadCatch m, Applicative m) => FilePath -> FilePath -> Err m () -compileAndOutput inputPath outputDir = - fileFormat inputPath >>= \case - Proof -> go proofReader - Tex -> go texReader +compileAndOutput inputPath outputDir = do + let p = pkgPath inputPath outputDir + htmlPath = p "index.html" + html <- join (compile <$> loadResources <*> texReader inputPath) + -- TODO: Dangerous to remove directories. Remove when you merge + + liftIO $ do + isDirectory p >>= flip when (removeTree p) + createDirectory False p + + liftIO (getDataFilePath "lib") >>= \l -> copyDirectory l p + liftIO $ do + forM_ ["src/js/proof.js", "src/css/proof.css"] $ \q -> + getDataFilePath q >>= \q' -> copyFile q' (p filename q) + T.writeFile (encodeString htmlPath) html where - getDataFilePath :: FilePath -> IO FilePath getDataFilePath = fmap decodeString . getDataFileName . encodeString - go reader = do - let p = pkgPath inputPath outputDir - htmlPath = p "index.html" - html <- join (compile <$> loadResources <*> reader inputPath) - -- TODO: Dangerous to remove directories. Remove when you merge - - liftIO $ do - isDirectory p >>= flip when (removeTree p) - createDirectory False p - - liftIO (getDataFilePath "lib") >>= \l -> copyDirectory l p - liftIO $ do - forM_ ["src/js/proof.js", "src/css/proof.css"] $ \q -> - getDataFilePath q >>= \q' -> copyFile q' (p filename q) - T.writeFile (encodeString htmlPath) html - -run inputPath outputDir = - runExceptT (compileAndOutput inputPath out) >>= \case - Left e -> putStrLn e - Right _ -> return () - where out = fromMaybe (directory inputPath) outputDir main :: IO () main = do @@ -144,3 +120,9 @@ main = do where fEvent = \case { Modified p _ -> p == inputPath; _ -> False } + run inputPath outputDir = + runExceptT (compileAndOutput inputPath out) >>= \case + Left e -> putStrLn e + Right _ -> return () + where out = fromMaybe (directory inputPath) outputDir + diff --git a/Parse.hs b/Parse.hs deleted file mode 100644 index d5259e1..0000000 --- a/Parse.hs +++ /dev/null @@ -1,152 +0,0 @@ -{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts, RankNTypes #-} -module Parse where - -import Types -import Utils --- import Text.Parsec hiding (label) -import Control.Monad -import Control.Monad.Except -import Prelude hiding (take) -import Data.Functor.Coproduct -import Data.Char (isSpace) -import DecoratedTex -import Parse.Common -import qualified Data.Text as T -import Text.LaTeX.Base.Parser -import Text.Parsec.Prim hiding (label) - --- TODO: Make macros --- TODO: Implement scope checking for labels - --- TODO: Figure out bad line numbers -texBlock :: Parsec String () (Block Ref) -texBlock = ( "texBlock") $ do - symbol "[|" - etex <- parseLaTeX . T.pack <$> manyTill anyChar (try (symbol "|]")) - tex <- either throwParseError pure etex - either fail pure (runExcept $ decorate tex) - where - throwParseError err = mkPT (\_ -> return (Consumed (return (Error err)))) - - -comment' :: Parser a -> Parser (a, Comment Ref) -comment' p = do - symbol "comment" - x <- p - text1 <- texBlock - whiteSpace - text2 <- optionMaybe texBlock - let (name, comm) = maybe (Nothing, text1) (\t2 -> (Just text1, t2)) text2 - return (x, Comment name comm) - -comment = snd <$> comment' (pure ()) - -listOf p = between (symbol "[" *> whiteSpace) (symbol "]") ((p <* whiteSpace) `sepBy` symbol ",") - -nodeData :: Parser NodeData -nodeData = optionMaybe (between (symbol "(") (symbol ")") label <* whiteSpace) - -keywordWithData :: String -> Parser NodeData -keywordWithData kw = symbol kw *> nodeData - -definition :: Parser (Raw DeclarationF) -definition = - Definition () <$> keywordWithData "definition" - <*> texBlock <* whiteSpace - <*> listOf (fmap left texBlock <|> fmap right comment) - -assumeProve :: Parser (TheoremStatement Ref) -assumeProve = do - symbol "assume" - assumptions <- listOf texBlock - whiteSpace - symbol "prove" - results <- listOf texBlock - return (AssumeProve assumptions results) - -theoremStatement :: Parser (TheoremStatement Ref) -theoremStatement = assumeProve - -maybeJustified :: Parser (MaybeJustifiedF () Ref) -maybeJustified = - (,) <$> (texBlock <* whiteSpace) - <*> optionMaybe (symbol "because" *> proof) - -suchThat :: Parser (Raw SuchThatF) -suchThat = do - symbol "such" >> symbol "that" - SuchThat <$> listOf maybeJustified - <*> optionMaybe (symbol "because" *> proof) - -take :: Parser (Raw StepF) -take = - Take () <$> keywordWithData "take" - <*> listOf texBlock - <*> optionMaybe suchThat - --- Add such that option for let -let_ :: Parser (Raw StepF) -let_ = - Let () <$> keywordWithData "let" - <*> listOf maybeJustified - <*> optionMaybe suchThat - -cases :: Parser (Raw StepF) -cases = - Cases () <$> keywordWithData "cases" <*> listOf oneCase - where - oneCase = do - symbol "case" - (,) <$> (texBlock <* whiteSpace) <*> proof - -claim :: Parser (Raw StepF) -claim = - Claim () <$> keywordWithData "claim" - <*> texBlock <* whiteSpace - <*> optionMaybe proof - -suppose :: Parser (Raw StepF) -suppose = - Suppose () <$> (keywordWithData "suppose") - <*> listOf texBlock <* symbol "then" -- TODO: Need whitespace here before symbol? - <*> listOf texBlock <* whiteSpace - <*> optionMaybe (symbol "because" *> proof) - --- TODO: Restructure parser for clearer parse-error messages. You have to --- commit to a particular type. E.g., if something deep in a `claim` fails, --- you'll get an error saying: unexpected "l", expecting "ases" - -step :: Parser (Raw StepF) -step = let_ - <|> suppose - <|> take - <|> try (uncurry (CommentStep ()) <$> comment' nodeData) - <|> try claim - <|> cases - -proof :: Parser (Raw ProofF) -proof = try (fmap Simple texBlock) <|> fmap Steps (listOf step) - -label :: Parser Label -label = Label <$> many (noneOf "%~#\\()[]{}") - --- TODO: Add support for in-file definition of theorem-kinds -theorem :: Parser (Raw DeclarationF) -theorem = do - kind <- symbol "theorem" <|> symbol "lemma" - mayLabel <- optionMaybe (between (symbol "(") (symbol ")") label) <* whiteSpace - name <- texBlock <* whiteSpace - statement <- theoremStatement <* whiteSpace - prf <- proof - pure (Theorem () mayLabel kind name statement prf) - -macros :: Parser (Raw DeclarationF) -macros = do - symbol "macros" - Macros . Block . pure . Raw . T.pack <$> literalText - where literalText = symbol "[|" *> manyTill anyChar (try (symbol "|]")) - -document :: Parser RawDocument -document = do - many ((theorem <|> macros <|> definition) <* whiteSpace) <* eof - diff --git a/TeXParser.hs b/TeXParser.hs deleted file mode 100644 index dadc5cf..0000000 --- a/TeXParser.hs +++ /dev/null @@ -1,332 +0,0 @@ - -{-# LANGUAGE OverloadedStrings #-} - --- | The /LaTeX/ parser. --- --- Use 'parseLaTeX' to parse a 'Text' containing /LaTeX/ code. --- If the 'Text' is in a file, you may want to use 'parseLaTeXFile'. --- Use this module together with "Text.LaTeX.Base.Syntax" to perform --- analysis and transformations of /LaTeX/ code. The parser ('parseLaTeX') --- is related with the renderer ('render') by the following property: --- --- /If @t :: Text@ is a syntactically valid LaTeX block, then:/ --- --- > fmap render (parseLaTeX t) == Right t --- --- This property says two things: --- --- * Given a valid LaTeX input, 'parseLaTeX' returns a 'LaTeX' value. --- * If the parsed value is again rendered, you get the initial input. --- --- In other words, 'parseLaTeX' is a partial function defined over the --- set of valid LaTeX files, and 'render' is its /left/ inverse. --- -module Text.LaTeX.Base.Parser ( - -- * The parser - parseLaTeX - , parseLaTeXFile - , latexParser - , latexBlockParser - -- * Parsing errors - , ParseError - , errorPos - , errorMessages - -- ** Error messages - , Message (..) - , messageString - -- ** Source positions - , SourcePos - , sourceLine - , sourceColumn - , sourceName - ) where - -import Text.Parsec hiding ((<|>),many) -import Text.Parsec.Text -import Text.Parsec.Error -import Data.Char (toLower,digitToInt) -import Data.Monoid -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import qualified Data.Text as T - -import Control.Applicative -import Control.Monad (unless) - --- import Text.LaTeX.Base.Render - --- | Parse a 'Text' sequence as a 'LaTeX' block. If it fails, it returns --- an error string. -parseLaTeX :: Text -> Either ParseError LaTeX -parseLaTeX t | T.null t = return TeXEmpty - | otherwise = parse latexParser "parseLaTeX input" t - --- | Read a file and parse it as 'LaTeX'. -parseLaTeXFile :: FilePath -> IO (Either ParseError LaTeX) -parseLaTeXFile fp = parse latexParser fp <$> readFileTex fp - --- | The 'LaTeX' parser. -latexParser :: Parser LaTeX -latexParser = mconcat <$> latexBlockParser `manyTill` eof - --- | Parser of a single 'LaTeX' constructor, no appending blocks. -latexBlockParser :: Parser LaTeX -latexBlockParser = foldr1 (<|>) - [ text "text" - , dolMath "inline math ($)" - , comment "comment" - , text2 "text2" - , try environment "environment" - , command "command" - ] --- Note: text stops on ']'; if the other parsers fail on the rest --- text2 handles it, starting with ']' - ------------------------------------------------------------------------- --- Text ------------------------------------------------------------------------- -text :: Parser LaTeX -text = do - mbC <- peekChar - case mbC of - Nothing -> fail "text: Empty input." - Just c | c `elem` "$%\\{]}" -> fail "not text" - | otherwise -> TeXRaw <$> takeTill (`elem` "$%\\{]}") - ------------------------------------------------------------------------- --- Text without stopping on ']' ------------------------------------------------------------------------- -text2 :: Parser LaTeX -text2 = do - _ <- char ']' - t <- try (text <|> return (TeXRaw T.empty)) - return $ TeXRaw (T.pack "]") <> t - ------------------------------------------------------------------------- --- Environment ------------------------------------------------------------------------- -environment :: Parser LaTeX -environment = anonym <|> env - -anonym :: Parser LaTeX -anonym = do - _ <- char '{' - l <- TeXBraces . mconcat <$> many latexBlockParser - _ <- char '}' - return l - -env :: Parser LaTeX -env = do - n <- char '\\' *> envName "begin" - sps <- many $ char ' ' - let lsps = if null sps then mempty else TeXRaw $ T.pack sps - as <- cmdArgs - b <- envBody n - return $ TeXEnv n (fromMaybe [] as) $ - case as of - Just [] -> lsps <> TeXBraces mempty <> b - Nothing -> lsps <> b - _ -> b - -envName :: String -> Parser String -envName k = do - _ <- string k - _ <- char '{' - n <- takeTill (== '}') - _ <- char '}' - return $ T.unpack n - -envBody :: String -> Parser LaTeX -envBody n = mconcat <$> (bodyBlock n) `manyTill` endenv - where endenv = try $ string ("\\end") >> spaces >> string ("{" <> n <> "}") - -bodyBlock :: String -> Parser LaTeX -bodyBlock n = do - c <- peekChar - case c of - Just _ -> latexBlockParser - _ -> fail $ "Environment '" <> n <> "' not finalized." - ------------------------------------------------------------------------- --- Command ------------------------------------------------------------------------- -command :: Parser LaTeX -command = do - _ <- char '\\' - mbX <- peekChar - case mbX of - Nothing -> return TeXEmpty - Just x -> if isSpecial x - then special - else do - c <- takeTill endCmd - -- if c `elem` ["begin","end"] - -- then fail $ "Command not allowed: " ++ T.unpack c - -- else maybe (TeXCommS $ T.unpack c) (TeXComm $ T.unpack c) <$> cmdArgs - maybe (TeXCommS $ T.unpack c) (TeXComm $ T.unpack c) <$> cmdArgs - ------------------------------------------------------------------------- --- Command Arguments ------------------------------------------------------------------------- -cmdArgs :: Parser (Maybe [TeXArg]) -cmdArgs = try (string "{}" >> return (Just [])) - <|> fmap Just (many1 cmdArg) - <|> return Nothing - -cmdArg :: Parser TeXArg -cmdArg = do - c <- char '[' <|> char '{' - let e = case c of - '[' -> "]" - '{' -> "}" - _ -> error "this cannot happen!" - b <- mconcat <$> manyTill latexBlockParser (string e) - case c of - '[' -> return $ OptArg b - '{' -> return $ FixArg b - _ -> error "this cannot happen!" - ------------------------------------------------------------------------- --- Special commands (consisting of one char) ------------------------------------------------------------------------- -special :: Parser LaTeX -special = do - x <- anyChar - case x of - '(' -> math Parentheses "\\)" - '[' -> math Square "\\]" - '{' -> lbrace - '}' -> rbrace - '|' -> vert - '\\' -> lbreak - _ -> commS [x] - ------------------------------------------------------------------------- --- Line break ------------------------------------------------------------------------- - -lbreak :: Parser LaTeX -lbreak = do - y <- try (char '[' <|> char '*' <|> return ' ') - case y of - '[' -> linebreak False - '*' -> do z <- try (char '[' <|> return ' ') - case z of - '[' -> linebreak True - _ -> return (TeXLineBreak Nothing True) - _ -> return (TeXLineBreak Nothing False) - -linebreak :: Bool -> Parser LaTeX -linebreak t = do m <- measure "measure" - _ <- char ']' - s <- try (char '*' <|> return ' ') - return $ TeXLineBreak (Just m) (t || s == '*') - -measure :: Parser Measure -measure = try (floating >>= unit) <|> (CustomMeasure . mconcat) <$> manyTill latexBlockParser (lookAhead $ char ']') - -unit :: Double -> Parser Measure -unit f = do - u1 <- anyChar - u2 <- anyChar - case map toLower [u1, u2] of - "pt" -> return $ Pt f - "mm" -> return $ Mm f - "cm" -> return $ Cm f - "in" -> return $ In f - "ex" -> return $ Ex f - "em" -> return $ Em f - _ -> fail "NaN" - ------------------------------------------------------------------------- --- Right or left brace or vertical ------------------------------------------------------------------------- -rbrace, lbrace,vert :: Parser LaTeX -lbrace = brace "{" -rbrace = brace "}" -vert = brace "|" - -brace :: String -> Parser LaTeX -brace = return . TeXCommS -- The same as commS? - -commS :: String -> Parser LaTeX -commS = return . TeXCommS - ------------------------------------------------------------------------- --- Math ------------------------------------------------------------------------- -dolMath :: Parser LaTeX -dolMath = do - _ <- char '$' - b <- mconcat <$> latexBlockParser `manyTill` char '$' - return $ TeXMath Dollar b - -math :: MathType -> String -> Parser LaTeX -math t eMath = do - b <- mconcat <$> latexBlockParser `manyTill` try (string eMath) - return $ TeXMath t b - ------------------------------------------------------------------------- --- Comment ------------------------------------------------------------------------- -comment :: Parser LaTeX -comment = do - _ <- char '%' - c <- takeTill (== '\n') - e <- atEnd - unless e (char '\n' >>= \_ -> return ()) - return $ TeXComment c - ------------------------------------------------------------------------- --- Helpers ------------------------------------------------------------------------- - -isSpecial :: Char -> Bool -isSpecial = (`elem` specials) - -endCmd :: Char -> Bool -endCmd c = notLowercaseAlph && notUppercaseAlph - where c' = fromEnum c - notLowercaseAlph = c' < fromEnum 'a' || c' > fromEnum 'z' - notUppercaseAlph = c' < fromEnum 'A' || c' > fromEnum 'Z' - - -specials :: String -specials = "'(),.-\"!^$&#{}%~|/:;=[]\\` " - -peekChar :: Parser (Maybe Char) -peekChar = Just <$> (try $ lookAhead anyChar) <|> pure Nothing - -atEnd :: Parser Bool -atEnd = (eof *> pure True) <|> pure False - -takeTill :: (Char -> Bool) -> Parser Text -takeTill p = T.pack <$> many (satisfy (not . p)) - --- Parsing doubles --- --- Code for 'floating', 'fractExponent', and 'sign' comes from parsers package: --- --- http://hackage.haskell.org/package/parsers --- - -floating :: Parser Double -floating = decimal <**> fractExponent - -fractExponent :: Parser (Integer -> Double) -fractExponent = (\fract expo n -> (fromInteger n + fract) * expo) <$> fraction <*> option 1.0 exponent' - <|> (\expo n -> fromInteger n * expo) <$> exponent' where - fraction = foldr op 0.0 <$> (char '.' *> (some digit "fraction")) - op d f = (f + fromIntegral (digitToInt d))/10.0 - exponent' = ((\f e -> power (f e)) <$ oneOf "eE" <*> sign <*> (decimal "exponent")) "exponent" - power e - | e < 0 = 1.0/power(-e) - | otherwise = fromInteger (10^e) - -decimal :: Parser Integer -decimal = read <$> many1 digit - -sign :: Parser (Integer -> Integer) -sign = negate <$ char '-' - <|> id <$ char '+' - <|> pure id diff --git a/example.proof b/example.proof deleted file mode 100644 index 977cf30..0000000 --- a/example.proof +++ /dev/null @@ -1,47 +0,0 @@ -macros [| - \newcommand{\bz}{\mathbb{Z}} - \newcommand{\bq}{\mathbb{Q}} -|] - -definition [|irrational|] [ - [|A real number $x$ is said to be irrational if $x \notin \bq$|] -] - -theorem (root2irrat) [|$\sqrt{2}$ is irrational|] - assume [ - [| $sqrt{2} \in \bq$ |] - ] prove [ - [| $\bot$ |] - ] - - [ claim [|It suffices to show that assuming $\sqrt{2} \in \bq$ leads to absurdity|] - [|Definition of irrational|] - , take [ - [|$n, m \in \bz$|] - ] such that [ - [| $\gcd(n, m) = 1$ and $n / m = \sqrt{2}$ |] because [ - take [ - [| $p, q \in \bz$ |] - ] such that [ - [| $p/q = \sqrt{2}$ |] because [| Assumed $\sqrt{2} \in \bq$, definition of $\bq$ |] - ], - - let [ - [|$n = p/\gcd(p, q)$|], - [|$m = q/\gcd(p, q)$|] - ], - - claim [| $n/m = \sqrt{2}$ |] [| Simple algebra |], - claim [| $\gcd(n, m) = 1$ |] [||] - ] - ] - - , claim [| $2$ divides $n$ |] [| $p^2 = 2q^2$ |] - , claim [| $2$ divides $m$ |] [] - ] - -lemma [|foo is bar|] - assume [[| foo|]] - prove [[| is bar|]] - [| See proof of \gref{root2irrat}. |] -