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 | infixr 7 :>
 17 |
 18 | public export
 19 | data Stack : Bool -> (s : List Type -> Type) -> List Type -> Type where
 20 |   Nil  : Stack False s []
 21 |   (:>) : (st : s ts) -> Stack b s ts -> Stack True s []
 22 |   (::) : (v : t)     -> Stack b s ts -> Stack False s (t::ts)
 23 |
 24 | public export %inline
 25 | push : {0 s : _} -> s [t] -> (v : t) -> Stack b s [] -> Stack True s []
 26 | push st v stck = st :> v :: stck
 27 |
 28 | --------------------------------------------------------------------------------
 29 | -- Mutable, Dependent Parser State
 30 | --------------------------------------------------------------------------------
 31 |
 32 | public export
 33 | record DStack (s : List Type -> Type) (e : Type) (q : Type) where
 34 |   [search q]
 35 |   constructor S
 36 |   line_      : Ref q Nat
 37 |   col_       : Ref q Nat
 38 |   positions_ : Ref q (SnocList Position)
 39 |   strings_   : Ref q (SnocList String)
 40 |   stack_     : Ref q (Stack True s [])
 41 |   error_     : Ref q (Maybe $ BoundedErr e)
 42 |   bytes_     : Ref q ByteString
 43 |
 44 | ||| Initializes a new parser stack.
 45 | export
 46 | init : Stack True s [] -> F1 q (DStack s e q)
 47 | init st = T1.do
 48 |   ln <- ref1 Z
 49 |   cl <- ref1 Z
 50 |   ps <- ref1 [<]
 51 |   ss <- ref1 [<]
 52 |   sk <- ref1 st
 53 |   er <- ref1 Nothing
 54 |   bs <- ref1 empty
 55 |   pure (S ln cl ps ss sk er bs)
 56 |
 57 | export %inline
 58 | HasStack (DStack s e) (Stack True s []) where
 59 |   stack = stack_
 60 |
 61 | export %inline
 62 | HasError (DStack s e) e where
 63 |   error = error_
 64 |
 65 | export %inline
 66 | HasPosition (DStack s e) where
 67 |   line = line_
 68 |   col  = col_
 69 |   positions = positions_
 70 |
 71 | export %inline
 72 | HasBytes (DStack s e) where
 73 |   bytes = bytes_
 74 |
 75 | export %inline
 76 | HasStringLits (DStack s e) where
 77 |   strings = strings_
 78 |
 79 | public export
 80 | 0 StateAct : Type -> (s : List Type -> Type) -> Bits32 -> Type
 81 | StateAct q s r =
 82 |      {0 b : _}
 83 |   -> {0 ts : _}
 84 |   -> s ts
 85 |   -> Stack b s ts
 86 |   -> F1 q (Index r)
 87 |
 88 | parameters {auto sk : DStack s e q}
 89 |
 90 |   export %inline
 91 |   dact : StateAct q s r -> F1 q (Index r)
 92 |   dact f t =
 93 |    let (st:>x) # t := read1 sk.stack_ t
 94 |     in f st x t
 95 |
 96 |   export %inline
 97 |   dput : s ts -> Cast (s ts) a => Stack b s ts -> F1 q a
 98 |   dput st x = writeAs sk.stack_ (st:>x) (cast st)
 99 |
100 |   export %inline
101 |   dpush : s [t] -> Cast (s [t]) a => t -> F1 q a
102 |   dpush st v t =
103 |    let stck # t := read1 sk.stack_ t
104 |     in writeAs sk.stack_ (st:>v::stck) (cast st) t
105 |
106 |   export %inline
107 |   derr : s [] -> Cast (s []) a => s ts -> Stack b s ts -> F1 q a
108 |   derr err st x = writeAs sk.stack_ (err:>st:>x) (cast err)
109 |