0 | ||| This module provides an experimental alternative
  1 | ||| to `Text.ILex.Stack` with a correctly typed parser
  2 | ||| stack.
  3 | module Text.ILex.DStack
  4 |
  5 | import Syntax.T1
  6 | import Text.ILex.Interfaces
  7 | import Text.ILex.Parser
  8 |
  9 | %default total
 10 |
 11 | --------------------------------------------------------------------------------
 12 | -- Dependent Parser Stack
 13 | --------------------------------------------------------------------------------
 14 |
 15 | export
 16 | infixl 7 :>
 17 |
 18 | public export
 19 | data Stack : Bool -> (s : SnocList Type -> Type) -> SnocList Type -> Type where
 20 |   Lin  : Stack False s [<]
 21 |   (:>) : Stack b s ts -> (st : s ts) -> Stack True s [<]
 22 |   (:<) : Stack b s ts -> (v : t) -> Stack False s (ts:<t)
 23 |
 24 | public export %inline
 25 | push : {0 s : _} -> Stack b s [<] -> (v : t) -> s [<t] -> Stack True s [<]
 26 | push stck v st = stck :< v :> st
 27 |
 28 | --------------------------------------------------------------------------------
 29 | -- Mutable, Dependent Parser State
 30 | --------------------------------------------------------------------------------
 31 |
 32 | public export
 33 | record DStack (s : SnocList Type -> Type) (e : Type) (q : Type) where
 34 |   [search q]
 35 |   constructor S
 36 |   -- Position and token bounds
 37 |   bufSize_    : Nat
 38 |   prev_       : ByteString
 39 |   cur_        : IBuffer bufSize_
 40 |   prevOffset_ : Nat
 41 |   curOffset_  : Nat
 42 |   from_       : Ref q (LTENat bufSize_)
 43 |   till_       : Ref q (LTENat bufSize_)
 44 |   positions_  : Ref q (SnocList BytePos)
 45 |
 46 |   strings_    : Ref q (SnocList String)
 47 |   stack_      : Ref q (Stack True s [<])
 48 |   error_      : Ref q (Maybe $ BBErr e)
 49 |
 50 | ||| Initializes a new parser stack.
 51 | export
 52 | init : Stack True s [<] -> (n : Nat) -> IBuffer n -> F1 q (DStack s e q)
 53 | init st n buf = T1.do
 54 |   rf <- ref1 (first n)
 55 |   rt <- ref1 (first n)
 56 |   ps <- ref1 [<]
 57 |   ss <- ref1 [<]
 58 |   sk <- ref1 st
 59 |   er <- ref1 Nothing
 60 |   pure (S n empty buf 0 0 rf rt ps ss sk er)
 61 |
 62 | export %inline
 63 | HasBytes (DStack s e) where
 64 |   bufSize    = bufSize_
 65 |   prev       = prev_
 66 |   cur        = cur_
 67 |   prevOffset = prevOffset_
 68 |   curOffset  = curOffset_
 69 |   from       = from_
 70 |   till       = till_
 71 |   positions  = positions_
 72 |   copy s o bs buf rf rt sk =
 73 |     { bufSize_    := s
 74 |     , cur_        := buf
 75 |     , prev_       := bs
 76 |     , prevOffset_ := o
 77 |     , curOffset_  := o + bs.size
 78 |     , from_       := rf
 79 |     , till_       := rt
 80 |     } sk
 81 |
 82 | export %inline
 83 | HasStack (DStack s e) (Stack True s [<]) where
 84 |   stack = stack_
 85 |
 86 | export %inline
 87 | HasBBErr (DStack s e) e where
 88 |   error = error_
 89 |
 90 | export %inline
 91 | HasStringLits (DStack s e) where
 92 |   strings = strings_
 93 |
 94 | public export
 95 | 0 StateAct : Type -> (s : SnocList Type -> Type) -> Bits32 -> Type
 96 | StateAct q s r =
 97 |      {0 b : _}
 98 |   -> {0 ts : _}
 99 |   -> s ts
100 |   -> Stack b s ts
101 |   -> F1 q (Index r)
102 |
103 | parameters {auto sk : DStack s e q}
104 |
105 |   export %inline
106 |   dact : StateAct q s r -> F1 q (Index r)
107 |   dact f t =
108 |    let (x:>st) # t := read1 sk.stack_ t
109 |     in f st x t
110 |
111 |   export %inline
112 |   dput : s ts -> Cast (s ts) a => Stack b s ts -> F1 q a
113 |   dput st x = writeAs sk.stack_ (x:>st) (cast st)
114 |
115 |   export %inline
116 |   dpush0 : s [<] -> Cast (s [<]) a => F1 q a
117 |   dpush0 st t =
118 |    let stck # t := read1 sk.stack_ t
119 |     in writeAs sk.stack_ (stck:>st) (cast st) t
120 |
121 |   export %inline
122 |   dpush : s [<t] -> Cast (s [<t]) a => t -> F1 q a
123 |   dpush st v t =
124 |    let stck # t := read1 sk.stack_ t
125 |     in writeAs sk.stack_ (stck:<v:>st) (cast st) t
126 |
127 |   export %inline
128 |   derr : s [<] -> Cast (s [<]) a => Stack b s ts -> s ts -> F1 q a
129 |   derr err st x = writeAs sk.stack_ (st:>x:>err) (cast err)
130 |