0 | module Parser.Unlit
  1 |
  2 | import Libraries.Utils.Path
  3 | import public Libraries.Text.Literate
  4 | import Data.String
  5 | import Data.List1
  6 | import Data.Maybe
  7 |
  8 | %default total
  9 |
 10 | public export
 11 | data LiterateModes = Bird | Org | CMark
 12 |
 13 | export
 14 | styleBird : LiterateStyle
 15 | styleBird = MkLitStyle Nil [">", "<"] [".lidr"]
 16 |
 17 | export
 18 | styleOrg : LiterateStyle
 19 | styleOrg = MkLitStyle
 20 |               [ ("#+BEGIN_SRC idris","#+END_SRC")
 21 |               , ("#+begin_src idris","#+end_src")
 22 |               , ("#+BEGIN_COMMENT idris","#+END_COMMENT")
 23 |               , ("#+begin_comment idris","#+end_comment")]
 24 |               ["#+IDRIS:"]
 25 |               [".org"]
 26 |
 27 | export
 28 | styleCMark : LiterateStyle
 29 | styleCMark = MkLitStyle
 30 |               [("```idris", "```"), ("~~~idris", "~~~"), ("<!-- idris", "-->")]
 31 |               Nil
 32 |               [".md", ".markdown", ".dj"]
 33 |
 34 | export
 35 | styleTeX : LiterateStyle
 36 | styleTeX = MkLitStyle
 37 |               [("\\begin{code}", "\\end{code}"), ("\\begin{hidden}", "\\end{hidden}")]
 38 |               Nil
 39 |               [".tex", ".ltx"]
 40 |
 41 | export
 42 | styleTypst : LiterateStyle
 43 | styleTypst = MkLitStyle
 44 |                [("```idris", "```"), ("/* idris", "*/")]
 45 |                Nil
 46 |                [".typ"]
 47 |
 48 |
 49 | supportedStyles : List LiterateStyle
 50 | supportedStyles = [styleBird, styleOrg, styleCMark, styleTeX, styleTypst]
 51 |
 52 | ||| Return the list of extensions used for literate files.
 53 | export
 54 | listOfExtensionsLiterate : List String
 55 | listOfExtensionsLiterate
 56 |   = do let exts = concatMap file_extensions supportedStyles
 57 |        pfx <- [ "", ".idr", ".lidr"]
 58 |        ext <- exts
 59 |        pure (pfx ++ ext)
 60 |
 61 | ||| Are we dealing with a valid literate file name, if so return the base name and used extension.
 62 | export
 63 | hasLitFileExt : (fname : String) -> Maybe (String, String)
 64 | hasLitFileExt fname =
 65 |   do let toExtension = concatMap ("." ++)
 66 |      -- split the extensions off a file
 67 |      -- e.g. "Cool.shared.org.lidr" becomes ("Cool", ["shared", "org", "lidr"])
 68 |      let (bn, exts) = splitExtensions fname
 69 |      flip choiceMap listOfExtensionsLiterate $ \ candidate =>
 70 |        do -- take candidate apart e.g. ".org.lidr" becomes ["org", "lidr"]
 71 |           -- we assume the candidate starts with a "." and so the first string
 72 |           -- should be empty
 73 |           let ("" ::: chunks) = map pack $ split ('.' ==) (unpack candidate)
 74 |             | _ => err
 75 |           -- check ["org", "lidr"] is a suffix of the files' extensions and get
 76 |           -- back (["shared"], ["org", "lidr"])
 77 |           (nm, exts) <- suffixOfBy (\ v, w => v <$ guard (v == w)) chunks exts
 78 |           -- return the basename extended with the leftover extensions, paired with the match
 79 |           -- e.g. ("Cool.shared", ".org.lidr")
 80 |           pure (bn ++ toExtension nm, toExtension exts)
 81 |
 82 |   where
 83 |
 84 |     err : a
 85 |     err = assert_total
 86 |         $ idris_crash #"Internal error: all literate extensions should start with a ".""#
 87 |
 88 | ||| Are we dealing with a valid literate file name, if so return the identified style.
 89 | export
 90 | isLitFile : String -> Maybe LiterateStyle
 91 | isLitFile fname = choiceMap isStyle supportedStyles
 92 |
 93 |   where
 94 |    hasSuffix : String -> Bool
 95 |    hasSuffix ext = isSuffixOf ext fname
 96 |
 97 |    isStyle : LiterateStyle -> Maybe LiterateStyle
 98 |    isStyle style =
 99 |      if any hasSuffix (file_extensions style)
100 |       then Just style
101 |       else Nothing
102 |
103 | ||| Check if the line is that from a literate style.
104 | export
105 | isLitLine : String -> (Maybe String, String)
106 | isLitLine str
107 |     = fromMaybe (Nothing, str) walk
108 |   where
109 |     try : LiterateStyle -> Maybe (Maybe String, String)
110 |     try style
111 |       = case isLiterateLine style str of
112 |           (Just l, s) => Just (Just l, s)
113 |           _           => Nothing
114 |
115 |     walk : Maybe (Maybe String, String)
116 |     walk = choiceMap try supportedStyles
117 |
118 | export
119 | unlit : Maybe LiterateStyle -> String -> Either LiterateError String
120 | unlit Nothing  str = Right str
121 | unlit (Just s) str = unlit s str
122 |
123 | export
124 | relit : Maybe String -> String -> String
125 | relit Nothing     str = str
126 | relit (Just mark) str = unwords [mark, str]
127 |