@@ -0,0 +1,132 @@
1+||| A simple module to process 'literate' documents.
2+|||
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..
10+|||
11+module Text.Literate
12+
13+import Text.Lexer
14+
15+import Data.List.Views
16+
17+%default total
18+
19+untilEOL : Recognise False
20+untilEOL = manyTill any (is '\n')
21+
22+line : String -> Lexer
23+line s = exact s <+> untilEOL
24+
25+block : String -> String -> Lexer
26+block s e = exact s <+> manyTill any (exact e)
27+
28+data Token = CodeBlock String String String
29+ | Any String
30+ | CodeLine String String
31+
32+Show (Token) where
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]
36+
37+rawTokens : (delims : List (String, String))
38+ -> (markers : List String)
39+ -> TokenMap (Token)
40+rawTokens delims ls =
41+ map (\(l,r) => (block l r, CodeBlock l r)) delims
42+ ++ map (\m => (line m, CodeLine m)) ls
43+ ++ [(any, Any)]
44+
45+||| Merge the tokens into a single source file.
46+reduce : List (TokenData Token) -> String -> String
47+reduce [] acc = acc
48+reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest acc
49+
50+reduce (MkToken _ _ (CodeLine m src) :: rest) acc = reduce rest (acc ++ (substr (length m) (length src) src))
51+
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)
57+
58+-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
59+
60+
61+public export
62+record LiterateError where
63+ constructor MkLitErr
64+ line : Int
65+ column : Int
66+ input : String
67+
68+||| Description of literate styles.
69+|||
70+||| A 'literate' style comprises of
71+|||
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`.
75+|||
76+||| Some example specifications:
77+|||
78+||| + Bird Style
79+|||
80+|||```
81+|||MkLitStyle Nil [">", "<"] Nil
82+|||```
83+|||
84+||| + Literate Haskell (for LaTeX)
85+|||
86+|||```
87+|||MkLitStyle [("\\begin{code}", "\\end{code}"),("\\begin{spec}","\\end{spec}")]
88+||| Nil
89+||| ["lhs", "tex"]
90+|||```
91+|||
92+||| + OrgMode
93+|||
94+|||```
95+|||MkLitStyle [("#+BEGIN_SRC idris","#+END_SRC"), ("#+COMMENT idris","#+END_COMMENT")]
96+||| ["#+IDRIS:"]
97+||| ["org"]
98+|||```
99+|||
100+public export
101+record LiterateStyle where
102+ constructor MkLitStyle
103+ ||| The pairs of start and end tags for code blocks.
104+ deliminators : List (String, String)
105+
106+ ||| Line markers that indicate a line contains code.
107+ line_markers : List String
108+
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
111+ ||| files.
112+ file_extensions : List String
113+
114+||| Given a 'literate specification' extract the code from the
115+||| literate source file (`litStr`) that follows the presented style.
116+|||
117+||| @specification The literate specification to use.
118+||| @litStr The literate source file.
119+|||
120+||| Returns a `LiterateError` if the literate file contains malformed
121+||| code blocks or code lines.
122+|||
123+export
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)
131+
132+-- --------------------------------------------------------------------- [ EOF ]