
   0 | module Text.ILex.Stack
   1 | 
   2 | import Data.Linear.Ref1
   3 | import Syntax.T1
   4 | import Text.ByteBounds
   5 | import Text.ILex.Derive
   6 | import Text.ILex.Interfaces
   7 | import Text.ILex.Parser
   8 | import Text.ILex.Util
   9 | import Text.ParseError
  10 | 
  11 | %hide Prelude.(>>)
  12 | %hide Prelude.(>>=)
  13 | %hide Prelude.pure
  14 | %default total
  15 | %language ElabReflection
  16 | 
  17 | --------------------------------------------------------------------------------
  18 | -- General Purpose Stack
  19 | --------------------------------------------------------------------------------
  20 | 
  21 | ||| A general-purpose mutable parser stack that can be used in many common
  22 | ||| situation, such as when needing just a lexer or wanting to parse
  23 | ||| a single value of a simple type.
  24 | |||
  25 | ||| For concrete usage examples, see ilex-json and ilex-toml, which both
  26 | ||| make use of this type as their mutable parser state.
  27 | |||
  28 | ||| If you are writing a parser for something complex such as a programming
  29 | ||| language, you're probably going to need quite a few custom fields, so
  30 | ||| feel free to come up with your own.
  31 | public export
  32 | record Stack (e,a : Type) (r : Bits32) (q : Type) where
  33 |   [search q]
  34 |   constructor S
  35 |   -- Position and token bounds
  36 |   prev_      : Ref q ByteString
  37 |   cur_       : Ref q ByteString
  38 |   offset_    : Ref q Nat
  39 |   relpos_    : Ref q Integer
  40 |   len_       : Ref q Nat
  41 |   positions_ : Ref q (SnocList BytePos)
  42 | 
  43 |   -- Custom stack type
  44 |   stack_     : Ref q a
  45 | 
  46 |   -- Current state
  47 |   state_     : Ref q (Index r)
  48 | 
  49 |   -- Working with string literals
  50 |   strings_   : Ref q (SnocList String)
  51 | 
  52 |   -- Error handling
  53 |   error_     : Ref q (Maybe $ BBErr e)
  54 | 
  55 | %runElab derive "Stack" [FullStack]
  56 | 
  57 | ||| Initializes a new parser stack.
  58 | export
  59 | init : (0 p : 0 < r) => a -> F1 q (Stack e a r q)
  60 | init v = T1.do
  61 |   pr <- ref1 empty
  62 |   fl <- ref1 empty
  63 |   ro <- ref1 Z
  64 |   rr <- ref1 0
  65 |   ll <- ref1 Z
  66 |   ps <- ref1 [<]
  67 |   sk <- ref1 v
  68 |   st <- ref1 (I 0)
  69 |   ss <- ref1 [<]
  70 |   er <- ref1 Nothing
  71 |   pure (S pr fl ro rr ll ps sk st ss er)
  72 | 
  73 | --------------------------------------------------------------------------------
  74 | -- Lexer
  75 | --------------------------------------------------------------------------------
  76 | 
  77 | public export
  78 | 0 Tok : Type -> Type
  79 | Tok = ByteBounded
  80 | 
  81 | public export
  82 | 0 Toks : Type -> Type
  83 | Toks = List . Tok
  84 | 
  85 | public export
  86 | 0 Skot : Type -> Type
  87 | Skot = SnocList . ByteBounded
  88 | 
  89 | public export
  90 | 0 L1 : (q,e : Type) -> (a : Type) -> Type
  91 | L1 q e a = P1 q (BBErr e) (Toks a)
  92 | 
  93 | public export
  94 | 0 Lexer : (e : Type) -> Type -> Type
  95 | Lexer e a = {0 q : Type} -> L1 q e a
  96 | 
  97 | parameters {auto hb   : HasBytes s}
  98 |            {auto hs   : HasStack s (Skot a)}
  99 |            (x         : RExp True)
 100 |            {auto 0 lt : 0 < r}
 101 | 
 102 |   export %inline
 103 |   pushBounded : s q => a -> F1 q (Index r)
 104 |   pushBounded v = bounded' v >>= \b => pushStackAs b 0
 105 | 
 106 |   export %inline
 107 |   tok : a -> (RExp True, Step q r s)
 108 |   tok v = step x (pushBounded v)
 109 | 
 110 |   export %inline
 111 |   byteTok : (ByteString -> a) -> (RExp True, Step q r s)
 112 |   byteTok f = bytes x (pushBounded . f)
 113 | 
 114 |   export %inline
 115 |   stringTok : (String -> a) -> (RExp True, Step q r s)
 116 |   stringTok f = string x (pushBounded . f)
 117 | 
 118 | export
 119 | lexEOI :
 120 |      {auto 0 lt : 0 < r}
 121 |   -> {auto stk : HasStack s (SnocList a)}
 122 |   -> {auto err : HasBBErr s e}
 123 |   -> {auto bts : HasBytes s}
 124 |   -> Index r
 125 |   -> s q
 126 |   -> F1 q (Either (BBErr e) $ List a)
 127 | lexEOI i sk =
 128 |   if i == Ini
 129 |      then getList (stack sk) >>= pure . Right
 130 |      else unexpected [] sk >>= pure . Left
 131 | 
 132 | export
 133 | lexer : {r : _} -> (0 lt : 0 < r) => Steps q r (Stack e (Skot a) r) -> L1 q e a
 134 | lexer m = P Ini (init [<]) (lex1 [E Ini $ dfa m]) snocChunk (errs []) lexEOI
 135 | 
 136 | --------------------------------------------------------------------------------
 137 | -- Values
 138 | --------------------------------------------------------------------------------
 139 | 
 140 | %runElab deriveParserState "VSz" "VST" ["VIni", "VErr", "VDone"]
 141 | 
 142 | ||| Description of lexicographic tokens
 143 | public export
 144 | data Token : (e, a : Type) -> Type where
 145 |   ||| Marks a terminal state that does not produce a token.
 146 |   ||| This can be used for comments or whitespace that should be
 147 |   ||| ignored.
 148 |   Ignore : Token e a
 149 | 
 150 |   ||| A constant token that allows us to emit a value directly.
 151 |   Const  : a -> Token e a
 152 | 
 153 |   ||| A token that needs to be parsed from its corresponding bytestring.
 154 |   Txt    : (String -> Either e a) -> Token e a
 155 | 
 156 |   ||| A token that needs to be parsed from its corresponding bytestring.
 157 |   Bytes  : (ByteString -> Either e a) -> Token e a
 158 | 
 159 | export %inline
 160 | const : a -> Token e a
 161 | const = Const
 162 | 
 163 | export %inline
 164 | txt : (String -> a) -> Token e a
 165 | txt f = Txt (Right . f)
 166 | 
 167 | export %inline
 168 | bytes : (ByteString -> a) -> Token e a
 169 | bytes f = Bytes (Right . f)
 170 | 
 171 | toStep :
 172 |      (RExpOf True b, Token e a)
 173 |   -> (RExpOf True b, Step q VSz (Stack e (Maybe a) VSz))
 174 | toStep (x,c) =
 175 |   case c of
 176 |     Ignore  => step' x VIni
 177 |     Const v => step x (putStackAs (Just v) VDone)
 178 |     Txt f   =>
 179 |       string x $ \s => case f s of
 180 |         Right v => putStackAs (Just v) VDone
 181 |         Left e  => failHere (Custom e) VErr
 182 |     Bytes f =>
 183 |       bytes x $ \s => case f s of
 184 |         Right v => putStackAs (Just v) VDone
 185 |         Left e  => failHere (Custom e) VErr
 186 | 
 187 | ignore :
 188 |      (RExpOf True b, Token e a)
 189 |   -> Maybe (RExpOf True b, Step q VSz (Stack e (Maybe a) VSz))
 190 | ignore (x,Ignore) = Just $ step' x VDone
 191 | ignore _          = Nothing
 192 | 
 193 | valEOI : VST -> Stack e (Maybe a) VSz q -> F1 q (Either (BBErr e) a)
 194 | valEOI i sk =
 195 |   if i == VDone || i == VIni
 196 |      then replace1 sk.stack_ Nothing >>= \case
 197 |             Just v  => pure (Right v)
 198 |             Nothing => unexpected [] sk >>= pure . Left
 199 |      else unexpected [] sk >>= pure . Left
 200 | 
 201 | public export
 202 | 0 PVal1 : (q,e : Type) -> (a : Type) -> Type
 203 | PVal1 q e a = P1 q (BBErr e) a
 204 | 
 205 | ||| Parser for simple values based on regular expressions.
 206 | export
 207 | value : Maybe a -> TokenMap (Token e a) -> PVal1 q e a
 208 | value mv m =
 209 |  let iniSteps  := E VIni $ dfa (map toStep m)
 210 |      doneSteps := E VDone $ dfa (mapMaybe ignore m)
 211 |      states    := lex1 [iniSteps, doneSteps]
 212 |   in P VIni (init mv) states noChunk (errs []) valEOI
 213 |