src/Idris/Unlit.hs · Idris-dev

git.iko.soy/Idris-dev

on master help sign in

42 lines 1.5 kB history raw

1{-|

2Module : Idris.Unlit

3Description : Turn literate programs into normal programs.

5License : BSD3

6Maintainer : The Idris Community.

7-}

8module Idris.Unlit(unlit) where

10import Idris.Core.TT

12import Data.Char

14unlit :: FilePath -> String -> TC String

15unlit f s = do let s' = map ulLine (lines s)

16 check f 1 s'

17 return $ unlines (map snd s')

19data LineType = Prog | Blank | Comm

21ulLine :: String -> (LineType, String)

22ulLine ('>':' ':xs) = (Prog, ' ':' ':xs) -- Replace with spaces, otherwise text position numbers will be bogus.

23ulLine ('>':xs) = (Prog, ' ' :xs) -- The parser can deal with this, because /every/ (code) line is prefixed

24 -- with a '>'.

25ulLine xs | all isSpace xs = (Blank, "")

26-- make sure it's not a doc comment

27 | otherwise = (Comm, '-':'-':' ':'>':xs)

29check :: FilePath -> Int -> [(LineType, String)] -> TC ()

30check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)

31 check f (l+1) (b:cs)

32check f l [x] = return ()

33check f l [ ] = return ()

35-- Issue #1593 on the issue checker.

37-- https://github.com/idris-lang/Idris-dev/issues/1593

39chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

40chkAdj f l Prog Comm = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

41chkAdj f l Comm Prog = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

42chkAdj f l _ _ = return ()