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