@@ -0,0 +1,132 @@
1+||| A simple module to process 'literate' documents.
3+||| The underlying tokeniser is greedy. Once it identifies a line
4+||| marker it reads until the end of line, and once it recognises a
5+||| start block, it will consume until the next identifiable end
6+||| block. Thus, the input literate files must be well-formed w.r.t to
7+||| line markers and code blocks. A further restriction is that
8+||| literate documents cannot contain the markers within the
9+||| document's main text: This will confuse the lexer..
15+import Data.List.Views
19+untilEOL : Recognise False
20+untilEOL = manyTill any (is '\n')
22+line : String -> Lexer
23+line s = exact s <+> untilEOL
25+block : String -> String -> Lexer
26+block s e = exact s <+> manyTill any (exact e)
28+data Token = CodeBlock String String String
30+ | CodeLine String String
33+ show (CodeBlock l r x) = unwords ["CodeBlock", show (l,r), show x]
34+ show (Any x) = unwords ["Any", show x]
35+ show (CodeLine m x) = unwords ["CodeLine", show m, show x]
37+rawTokens : (delims : List (String, String))
38+ -> (markers : List String)
41+ map (\(l,r) => (block l r, CodeBlock l r)) delims
42+ ++ map (\m => (line m, CodeLine m)) ls
45+||| Merge the tokens into a single source file.
46+reduce : List (TokenData Token) -> String -> String
48+reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest acc
50+reduce (MkToken _ _ (CodeLine m src) :: rest) acc = reduce rest (acc ++ (substr (length m) (length src) src))
52+reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
53+ reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
54+ reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
55+ reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
56+ reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc rec) = reduce rest (acc ++ unlines srcs)
58+-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
62+record LiterateError where
68+||| Description of literate styles.
70+||| A 'literate' style comprises of
72+||| + a list of code block deliminators (`deliminators`);
73+||| + a list of code line markers (`line_markers`); and
74+||| + a list of known file extensions `file_extensions`.
76+||| Some example specifications:
81+|||MkLitStyle Nil [">", "<"] Nil
84+||| + Literate Haskell (for LaTeX)
87+|||MkLitStyle [("\\begin{code}", "\\end{code}"),("\\begin{spec}","\\end{spec}")]
95+|||MkLitStyle [("#+BEGIN_SRC idris","#+END_SRC"), ("#+COMMENT idris","#+END_COMMENT")]
101+record LiterateStyle where
102+ constructor MkLitStyle
103+ ||| The pairs of start and end tags for code blocks.
104+ deliminators : List (String, String)
106+ ||| Line markers that indicate a line contains code.
107+ line_markers : List String
109+ ||| Recognised file extensions. Not used by the module, but will be
110+ ||| of use when connecting to code that reads in the original source
112+ file_extensions : List String
114+||| Given a 'literate specification' extract the code from the
115+||| literate source file (`litStr`) that follows the presented style.
117+||| @specification The literate specification to use.
118+||| @litStr The literate source file.
120+||| Returns a `LiterateError` if the literate file contains malformed
121+||| code blocks or code lines.
124+extractCode : (specification : LiterateStyle)
125+ -> (litStr : String)
126+ -> Either LiterateError String
127+extractCode (MkLitStyle delims markers exts) str =
128+ case lex (rawTokens delims markers) str of
129+ (toks, (_,_,"")) => Right $ reduce toks ""
130+ (_, (l,c,i)) => Left (MkLitErr l c i)
132+-- --------------------------------------------------------------------- [ EOF ]