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' = 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'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines (forall a b. (a -> b) -> [a] -> [b]
map 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
' 'forall a. a -> [a] -> [a]
:Char
' 'forall a. a -> [a] -> [a]
:FilePath
xs)
ulLine (Char
'>':FilePath
xs) = (LineType
Prog, Char
' ' forall a. a -> [a] -> [a]
:FilePath
xs)
ulLine FilePath
xs | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
xs = (LineType
Blank, FilePath
"")
| Bool
otherwise = (LineType
Comm, Char
'-'forall a. a -> [a] -> [a]
:Char
'-'forall a. a -> [a] -> [a]
:Char
' 'forall a. a -> [a] -> [a]
:Char
'>'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 (forall a b. (a, b) -> a
fst (LineType, FilePath)
a) (forall a b. (a, b) -> a
fst (LineType, FilePath)
b)
FilePath -> Int -> [(LineType, FilePath)] -> TC ()
check FilePath
f (Int
lforall a. Num a => a -> a -> a
+Int
1) ((LineType, FilePath)
bforall a. a -> [a] -> [a]
:[(LineType, FilePath)]
cs)
check FilePath
f Int
l [(LineType, FilePath)
x] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
check FilePath
f Int
l [ ] = 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 = forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ 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)) forall t. Err' t
ProgramLineComment
chkAdj FilePath
f Int
l LineType
Comm LineType
Prog = forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ 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)) forall t. Err' t
ProgramLineComment
chkAdj FilePath
f Int
l LineType
_ LineType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()