
   0 | module Text.Regex.Printer
   1 | 
   2 | import Data.String
   3 | import Data.Vect.Extra
   4 | 
   5 | import Derive.Eq
   6 | import Derive.Ord
   7 | 
   8 | import Language.Reflection
   9 | import Language.Reflection.Derive
  10 | import Language.Reflection.Syntax
  11 | import Language.Reflection.Types
  12 | 
  13 | import Text.Regex.Interface
  14 | 
  15 | %default total
  16 | %language ElabReflection
  17 | 
  18 | data OpPri = Alt | Conseq | Postfix | Symbol
  19 | 
  20 | %runElab derive `{OpPri} [Eq, Ord]
  21 | 
  22 | export
  23 | data RegExpText a = RET OpPri String
  24 | 
  25 | tostr : (context : OpPri) -> RegExpText a -> String
  26 | tostr Postfix $ RET Postfix s = "(?:\{s})"
  27 | tostr outer   $ RET inner   s = if outer > inner then "(?:\{s})" else s
  28 | 
  29 | Cast (RegExpText a) (RegExpText b) where
  30 |   cast $ RET p s = RET p s
  31 | 
  32 | export
  33 | Functor RegExpText where
  34 |   map _ = cast
  35 | 
  36 | export
  37 | Applicative RegExpText where
  38 |   pure _ = RET Conseq ""
  39 |   l@(RET pl l') <*> r@(RET pr r') = do
  40 |     let sl = tostr Conseq l
  41 |     let sr = tostr Conseq r
  42 |     if null sl then cast r else
  43 |       if null sr then cast l else
  44 |         RET Conseq $ sl <+> sr
  45 | 
  46 | export
  47 | Alternative RegExpText where
  48 |   empty = RET Conseq #"\b\B"#
  49 |   l <|> r = RET Alt "\{tostr Alt l}|\{tostr Alt r}"
  50 | 
  51 | toHex : Int -> String
  52 | toHex = pack . go [] where
  53 |   ord0, ordA : Int
  54 |   ord0 = ord '0'
  55 |   ordA = ord 'A'
  56 |   go : List Char -> Int -> List Char
  57 |   go acc n = do
  58 |     let n' = n `div` 16
  59 |     let r = n `mod` 16
  60 |     let c = chr $ r + if r < 10 then ord0 else ordA
  61 |     let acc = c :: acc
  62 |     if n' > 0 then go acc $ assert_smaller n n' else acc
  63 | 
  64 | printChar : Char -> String
  65 | printChar '\n' = #"\n"#
  66 | printChar '\r' = #"\r"#
  67 | printChar '\t' = #"\t"#
  68 | printChar '\f' = #"\f"#
  69 | printChar '\v' = #"\v"#
  70 | printChar '\a' = #"\a"#
  71 | printChar '\\' = #"\\"#
  72 | printChar c = let ordC = ord c in
  73 |   if 0x20 <= ordC && ordC <= 0x7E then singleton c
  74 |     else if ordC <= 0xFF then "\\x\{toHex $ ordC `div` 16}\{toHex $ ordC `mod` 16}"
  75 |       else "\\x{\{toHex ordC}}"
  76 | 
  77 | test127 : (Char -> Bool) -> Vect 127 Bool
  78 | test127 f = allFins _ <&> f . chr . cast . finToNat
  79 | 
  80 | -- sorted from big to small
  81 | searchPosixClasses : List (String, Vect 127 Bool)
  82 | searchPosixClasses = map @{Compose} (test127 . charClass) $
  83 |   [ ("print", Print), ("graph", Graph), ("alnum", Alnum), ("alpha", Alpha), ("upper", Upper), ("lower", Lower)
  84 |   , ("xdigit", XDigit), ("digit", Digit), ("punct", Punct) , ("cntrl", Cntrl), ("space", Space), ("blank", Blank) ]
  85 | 
  86 | findAndCut : (a -> Bool) -> List a -> Maybe (List a, a)
  87 | findAndCut f []      = Nothing
  88 | findAndCut f (x::xs) = if f x then Just (xs, x) else findAndCut f xs
  89 | 
  90 | -- we can treat `a <= b` as logical implication of `a` to `b` when they're `Bool`s
  91 | calcPosClass : Vect 127 Bool -> (SnocList String, Vect 127 Bool)
  92 | calcPosClass orig = go searchPosixClasses orig [<] where
  93 |   go : List (String, Vect 127 Bool) -> Vect 127 Bool -> SnocList String -> (SnocList String, Vect 127 Bool)
  94 |   go spc curr acc = case findAndCut (\(_, vs) => all (\(v, o) => v <= o) (zip vs orig) && any (\(v, c) => v && c) (zip vs curr)) spc of
  95 |     Just (spc, name, vs) => go spc (assert_smaller curr $ zipWith (\c, v => c && not v) curr vs) (acc :< name)
  96 |     Nothing => (acc, curr)
  97 | 
  98 | calcClass : Vect 127 Bool -> RegExpText a
  99 | calcClass vs = do
 100 |   let (pcls, pvs) = calcPosClass vs
 101 |   let (ncls, nvs) = calcPosClass $ not <$> vs
 102 |   let (pn, nn) = mapHom (let _ = Monoid.Additive in foldMap $ \b => if b then 1 else 0) (pvs, nvs)
 103 |   let (neg, cls, vs) = if pn <= nn then (False, pcls, pvs) else (True, ncls, nvs)
 104 |   let fin = concatMap (\cl => "[:\{cl}:]") cls ++ concatMap (\(b, n) => if b then printChar (chr $ cast $ finToNat n) else "") (toListI vs)
 105 |   if length fin == 0 then empty else
 106 |     if neg || length fin > 1
 107 |       then let neg : String := if neg then "^" else "" in RET Symbol "[\{neg}\{fin}]"
 108 |       else RET Symbol fin
 109 | 
 110 | export
 111 | Regex RegExpText where
 112 |   -- this implementation only takes behaviour on ASCII symbols into account
 113 |   sym' = calcClass . test127 . (isJust .)
 114 |   char = RET Symbol . singleton
 115 | 
 116 |   anyChar Line = RET Symbol "."
 117 |   anyChar Text = RET Symbol #"\X"#
 118 |   edge Line Start = RET Symbol "^"
 119 |   edge Line End   = RET Symbol "$"
 120 |   edge Text Start = RET Symbol #"\A"#
 121 |   edge Text End   = RET Symbol #"\z"#
 122 | 
 123 |   wordBoundary True  True  = RET Symbol #"\b"#
 124 |   wordBoundary True  False = RET Symbol #"\<"#
 125 |   wordBoundary False True  = RET Symbol #"\>"#
 126 |   wordBoundary False False = RET Symbol #"\B"#
 127 | 
 128 |   string = RET Conseq
 129 | 
 130 |   withMatch $ RET _ s = RET Symbol "(\{s})"
 131 | 
 132 |   exists []        = empty
 133 |   exists [RET p s] = RET p s
 134 |   exists rs        = RET Alt $ joinBy "|" $ forget $ mapProperty (tostr Alt) rs
 135 | 
 136 |   opt  r = RET Postfix "\{tostr Postfix r}?"
 137 |   rep  r = RET Postfix "\{tostr Postfix r}*"
 138 |   rep1 r = RET Postfix "\{tostr Postfix r}+"
 139 |   repeatN       n r = RET Postfix "\{tostr Postfix r}{\{show n}}"
 140 |   repeatNOrMore n r = RET Postfix "\{tostr Postfix r}{\{show n},}"
 141 |   repeatNOrLess n r = RET Postfix "\{tostr Postfix r}{,\{show n}}"
 142 |   repeatNM    n m r = RET Postfix "\{tostr Postfix r}{\{show n},\{show m}}"
 143 | 
 144 | export
 145 | Interpolation (RegExpText a) where
 146 |   interpolate $ RET _ s = s
 147 |