git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Unlit.hs
33 lines 1.1 kB history raw
1module Idris.Unlit(unlit) where
3import Idris.Core.TT
4import Data.Char
6unlit :: FilePath -> String -> TC String
7unlit f s = do let s' = map ulLine (lines s)
8 check f 1 s'
9 return $ unlines (map snd s')
11data LineType = Prog | Blank | Comm
13ulLine :: String -> (LineType, String)
14ulLine ('>':' ':xs) = (Prog, xs)
15ulLine ('>':xs) = (Prog, xs)
16ulLine xs | all isSpace xs = (Blank, "")
17-- make sure it's not a doc comment
18 | otherwise = (Comm, '-':'-':' ':'>':xs)
20check :: FilePath -> Int -> [(LineType, String)] -> TC ()
21check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)
22 check f (l+1) (b:cs)
23check f l [x] = return ()
24check f l [] = return ()
26-- Issue #1593 on the issue checker.
27--
28-- https://github.com/idris-lang/Idris-dev/issues/1593
29--
30chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()
31chkAdj f l Prog Comm = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly
32chkAdj f l Comm Prog = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly
33chkAdj f l _ _ = return ()