module Parser.Unlit %default total exportisLitFile : String -> BoolisLitFile file = isSuffixOf ".lidr" file data LineType = Blank | Code | Text lineType : String -> (LineType, String)lineType str = if length str > 0  then    if assert_total (strHead str) == '>'       then (Code, assert_total (strTail str))       else         if all isSpace (unpack str)            then (Blank, str)            else (Text, str)  else (Blank, str) exportisLit : String -> (Bool, String)isLit str = case lineType str of               (Code, tail) => (True, tail)               _ => (False, str) exportunlit : Bool -> Bool -> String -> Either (List Int) Stringunlit lit enforce str = if lit  then let (_, lns, errors) = foldr unlit' (Blank, [], []) (lines str) in           if enforce              then case errors of                        [] => Right (unlines lns)                        _ => let l : Int = cast (length lns) in Left (map (l -) errors)              else Right (unlines lns)  else Right str where    unlit' : String -> (LineType, List String, List Int) -> (LineType, List String, List Int)    unlit' str (type, ls, errs) with (lineType str)      unlit' str (Code, ls, errs) | (Text, _) = (Text, "" :: ls, cast (length ls) :: errs)      unlit' str (Text, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, cast (length ls) :: errs)      unlit' str (type, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, errs)      unlit' str (type, ls, errs) | (new, s) = (new, "" :: ls, errs)