{-|
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 f :: FilePath
f s :: 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 1 [(LineType, FilePath)]
s'
               FilePath -> TC FilePath
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 ('>':' ':xs :: FilePath
xs)        = (LineType
Prog, ' 'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:' 'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs) -- Replace with spaces, otherwise text position numbers will be bogus.
ulLine ('>':xs :: FilePath
xs)            = (LineType
Prog, ' '    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 xs :: FilePath
xs | (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
xs = (LineType
Blank, "")
-- make sure it's not a doc comment
          | Bool
otherwise      = (LineType
Comm, '-'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:'-'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:' 'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:'>'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs)

check :: FilePath -> Int -> [(LineType, String)] -> TC ()
check :: FilePath -> Int -> [(LineType, FilePath)] -> TC ()
check f :: FilePath
f l :: Int
l (a :: (LineType, FilePath)
a:b :: (LineType, FilePath)
b:cs :: [(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
+1) ((LineType, FilePath)
b(LineType, FilePath)
-> [(LineType, FilePath)] -> [(LineType, FilePath)]
forall a. a -> [a] -> [a]
:[(LineType, FilePath)]
cs)
check f :: FilePath
f l :: Int
l [x :: (LineType, FilePath)
x] = () -> TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check f :: FilePath
f l :: Int
l [ ] = () -> TC ()
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 f :: FilePath
f l :: Int
l Prog 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, 0) (Int
l, 0)) Err
forall t. Err' t
ProgramLineComment --TODO: Span correctly
chkAdj f :: FilePath
f l :: Int
l Comm 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, 0) (Int
l, 0)) Err
forall t. Err' t
ProgramLineComment --TODO: Span correctly
chkAdj f :: FilePath
f l :: Int
l _    _    = () -> TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()