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)
ulLine ('>':xs :: FilePath
xs) = (LineType
Prog, ' ' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
xs)
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, "")
| 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 ()
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
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
chkAdj f :: FilePath
f l :: Int
l _ _ = () -> TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()