
   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 |   prev_      : Ref q ByteString
  38 |   cur_       : Ref q ByteString
  39 |   offset_    : Ref q Nat
  40 |   relpos_    : Ref q Integer
  41 |   len_       : Ref q Nat
  42 |   positions_ : Ref q (SnocList BytePos)
  43 | 
  44 |   strings_   : Ref q (SnocList String)
  45 |   stack_     : Ref q (Stack True s [<])
  46 |   error_     : Ref q (Maybe $ BBErr e)
  47 | 
  48 | ||| Initializes a new parser stack.
  49 | export
  50 | init : Stack True s [<] -> F1 q (DStack s e q)
  51 | init st = T1.do
  52 |   pr <- ref1 empty
  53 |   fl <- ref1 empty
  54 |   ro <- ref1 Z
  55 |   rr <- ref1 0
  56 |   ll <- ref1 Z
  57 |   ps <- ref1 [<]
  58 |   ss <- ref1 [<]
  59 |   sk <- ref1 st
  60 |   er <- ref1 Nothing
  61 |   pure (S pr fl ro rr ll ps ss sk er)
  62 | 
  63 | export %inline
  64 | HasBytes (DStack s e) where
  65 |   prev    = prev_
  66 |   cur     = cur_
  67 |   offset  = offset_
  68 |   relpos  = relpos_
  69 |   len     = len_
  70 |   positions = positions_
  71 | 
  72 | export %inline
  73 | HasStack (DStack s e) (Stack True s [<]) where
  74 |   stack = stack_
  75 | 
  76 | export %inline
  77 | HasBBErr (DStack s e) e where
  78 |   error = error_
  79 | 
  80 | export %inline
  81 | HasStringLits (DStack s e) where
  82 |   strings = strings_
  83 | 
  84 | public export
  85 | 0 StateAct : Type -> (s : SnocList Type -> Type) -> Bits32 -> Type
  86 | StateAct q s r =
  87 |      {0 b : _}
  88 |   -> {0 ts : _}
  89 |   -> s ts
  90 |   -> Stack b s ts
  91 |   -> F1 q (Index r)
  92 | 
  93 | parameters {auto sk : DStack s e q}
  94 | 
  95 |   export %inline
  96 |   dact : StateAct q s r -> F1 q (Index r)
  97 |   dact f t =
  98 |    let (x:>st) # t := read1 sk.stack_ t
  99 |     in f st x t
 100 | 
 101 |   export %inline
 102 |   dput : s ts -> Cast (s ts) a => Stack b s ts -> F1 q a
 103 |   dput st x = writeAs sk.stack_ (x:>st) (cast st)
 104 | 
 105 |   export %inline
 106 |   dpush0 : s [<] -> Cast (s [<]) a => F1 q a
 107 |   dpush0 st t =
 108 |    let stck # t := read1 sk.stack_ t
 109 |     in writeAs sk.stack_ (stck:>st) (cast st) t
 110 | 
 111 |   export %inline
 112 |   dpush : s [<t] -> Cast (s [<t]) a => t -> F1 q a
 113 |   dpush st v t =
 114 |    let stck # t := read1 sk.stack_ t
 115 |     in writeAs sk.stack_ (stck:<v:>st) (cast st) t
 116 | 
 117 |   export %inline
 118 |   derr : s [<] -> Cast (s [<]) a => Stack b s ts -> s ts -> F1 q a
 119 |   derr err st x = writeAs sk.stack_ (st:>x:>err) (cast err)
 120 |