{-|
Module      : Idris.Unlit
Description : Turn literate programs into normal programs.

License     : BSD3
Maintainer  : The Idris Community.
-}
module Idris.Unlit(unlit) where

import Idris.Core.TT

import Data.Char

unlit :: FilePath -> String -> TC String
unlit :: FilePath -> FilePath -> TC FilePath
unlit FilePath
f FilePath
s = do let s' :: [(LineType, FilePath)]
s' = (FilePath -> (LineType, FilePath))
-> [FilePath] -> [(LineType, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> (LineType, FilePath)
ulLine (FilePath -> [FilePath]
lines FilePath
s)
               FilePath -> Int -> [(LineType, FilePath)] -> TC ()
check FilePath
f Int
1 [(LineType, FilePath)]
s'
               FilePath -> TC FilePath
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> TC FilePath) -> FilePath -> TC FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines (((LineType, FilePath) -> FilePath)
-> [(LineType, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (LineType, FilePath) -> FilePath
forall a b. (a, b) -> b
snd [(LineType, FilePath)]
s')

data LineType = Prog | Blank | Comm

ulLine :: String -> (LineType, String)
ulLine :: FilePath -> (LineType, FilePath)
ulLine (Char
'>':Char
' ':FilePath
xs)        = (LineType
Prog, Char
' 'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:Char
' 'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs) -- Replace with spaces, otherwise text position numbers will be bogus.
ulLine (Char
'>':FilePath
xs)            = (LineType
Prog, Char
' '    Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs) -- The parser can deal with this, because /every/ (code) line is prefixed
                                                -- with a '>'.
ulLine FilePath
xs | (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
xs = (LineType
Blank, FilePath
"")
-- make sure it's not a doc comment
          | Bool
otherwise      = (LineType
Comm, Char
'-'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:Char
'-'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:Char
' 'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:Char
'>'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs)

check :: FilePath -> Int -> [(LineType, String)] -> TC ()
check :: FilePath -> Int -> [(LineType, FilePath)] -> TC ()
check FilePath
f Int
l ((LineType, FilePath)
a:(LineType, FilePath)
b:[(LineType, FilePath)]
cs) = do FilePath -> Int -> LineType -> LineType -> TC ()
chkAdj FilePath
f Int
l ((LineType, FilePath) -> LineType
forall a b. (a, b) -> a
fst (LineType, FilePath)
a) ((LineType, FilePath) -> LineType
forall a b. (a, b) -> a
fst (LineType, FilePath)
b)
                        FilePath -> Int -> [(LineType, FilePath)] -> TC ()
check FilePath
f (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((LineType, FilePath)
b(LineType, FilePath)
-> [(LineType, FilePath)] -> [(LineType, FilePath)]
forall a. a -> [a] -> [a]
:[(LineType, FilePath)]
cs)
check FilePath
f Int
l [(LineType, FilePath)
x] = () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check FilePath
f Int
l [ ] = () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- Issue #1593 on the issue checker.
--
--     https://github.com/idris-lang/Idris-dev/issues/1593
--
chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()
chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()
chkAdj FilePath
f Int
l LineType
Prog LineType
Comm = Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At (FilePath -> (Int, Int) -> (Int, Int) -> FC
FC FilePath
f (Int
l, Int
0) (Int
l, Int
0)) Err
forall t. Err' t
ProgramLineComment --TODO: Span correctly
chkAdj FilePath
f Int
l LineType
Comm LineType
Prog = Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At (FilePath -> (Int, Int) -> (Int, Int) -> FC
FC FilePath
f (Int
l, Int
0) (Int
l, Int
0)) Err
forall t. Err' t
ProgramLineComment --TODO: Span correctly
chkAdj FilePath
f Int
l LineType
_    LineType
_    = () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()