0 | module Text.ILex.Internal.Types

  2 | import public Text.ILex.RExp

  3 | import public Data.Linear.Ref1

  5 | import Data.Array.Core

  6 | import Data.Array.Index

  7 | import Data.Array.Mutable

  8 | import Data.Linear.Traverse1

  9 | import Data.Maybe

 10 | import Data.SortedMap

 11 | import Derive.Prelude

 12 | import Syntax.T1

 14 | %default total

 15 | %language ElabReflection

 27 | record NatMap1 (s,a : Type) where

 28 |   constructor NM1

 29 |   ref   : Ref s (n ** MArray s n (Maybe a))

 32 | empty : {default 256 size : Nat} -> (0 p : IsSucc size) => F1 s (NatMap1 s a)

 33 | empty = T1.do

 34 |   arr <- marray1 size Nothing

 35 |   ref <- ref1 (size ** arr)

 36 |   pure (NM1 ref)

 39 | lookup1 : Nat -> NatMap1 s a -> F1 s (Maybe a)

 40 | lookup1 n m =

 41 |   read1 m.ref >>= \(sz ** vs) =>

 42 |     case tryNatToFin n of

 43 |       Just x  => Core.get vs x

 44 |       Nothing => pure Nothing

 47 | lookupDflt1 : Nat -> Lazy a -> NatMap1 s a -> F1 s a

 48 | lookupDflt1 n dflt m =

 49 |   read1 m.ref >>= \(sz ** vs) =>

 50 |     case tryNatToFin n of

 51 |       Just x  => Core.get vs x >>= pure . fromMaybe dflt

 52 |       Nothing => pure dflt

 55 | delete1 : Nat -> NatMap1 s a -> F1' s

 56 | delete1 n m =

 57 |   read1 m.ref >>= \(sz ** vs) =>

 58 |     case tryNatToFin n of

 59 |       Just x  => Core.set vs x Nothing

 60 |       Nothing => pure ()

 63 | insert1 : Nat -> a -> NatMap1 s a -> F1' s

 64 | insert1 n v m = read1 m.ref >>= \(_ ** vs) => go vs

 65 |   where

 66 |     go : {sz : _} -> MArray s sz (Maybe a) -> F1' s

 67 |     go vs t =

 68 |       case tryNatToFin n of

 69 |         Just x  =>

 70 |          let _ # t := Core.set vs x (Just v) t

 71 |           in write1 m.ref (_ ** vs) t

 72 |         Nothing =>

 73 |          let vs2 # t := mgrow vs sz Nothing t

 74 |           in go (assert_smaller vs vs2) t

 77 | fromList1 : List (Nat,a) -> F1 s (NatMap1 s a)

 78 | fromList1 ps = T1.do

 79 |   m <- empty

 80 |   traverse1_ (\(k,v) => insert1 k v m) ps

 81 |   pure m

 84 | pairs1 : NatMap1 s a -> F1 s (List (Nat,a))

 85 | pairs1 m = read1 m.ref >>= \(sz ** vs) => go vs [<] sz

 86 |   where

 87 |     go :

 88 |          MArray s sz (Maybe a)

 89 |       -> SnocList (Nat,a)

 90 |       -> (n : Nat)

 91 |       -> {auto 0 lte : LTE n sz}

 92 |       -> F1 s (List (Nat,a))

 93 |     go vs sv 0     t = (sv <>> []) # t

 94 |     go vs sv (S k) t =

 95 |       case getNat vs k t of

 96 |         Just v  # t => go vs (sv:<(k,v)) k t

 97 |         Nothing # t => go vs sv k t

 99 | export %inline

100 | keys1 : NatMap1 s a -> F1 s (List Nat)

101 | keys1 m = map fst <$> pairs1 m

103 | export %inline

104 | values1 : NatMap1 s a -> F1 s (List a)

105 | values1 m = map snd <$> pairs1 m

111 | parameters {sz       : Nat}

112 |            (children : a -> List Nat)

113 |            (visited  : MArray s sz Bool)

114 |            (is,os    : MArray s sz (Maybe a))

116 |   covering

117 |   visit : List Nat -> F1' s

118 |   visit []      t = () # t

119 |   visit (x::xs) t =

120 |     case tryNatToFin x of

121 |       Nothing => visit xs t

122 |       Just k  => case Core.get visited k t of

123 |         True  # t => visit xs t

124 |         False # t =>

125 |          let _ # t := Core.set visited k True t

126 |           in case Core.get is k t of

127 |                Nothing   # t => visit xs t

128 |                Just node # t =>

129 |                 let _ # t := Core.set os k (Just node) t

130 |                  in visit (children node ++ xs) t

133 | connectedComponent : (a -> List Nat) -> Nat -> NatMap1 s a -> F1' s

134 | connectedComponent c n m =

135 |   read1 m.ref >>= \(sz ** is) => T1.do

136 |     vis <- marray1 sz False

137 |     os  <- marray1 sz Nothing

138 |     assert_total $ visit c vis is os [n]

139 |     write1 m.ref (sz ** os)

145 | public export

146 | 0 NSet : Type

147 | NSet = List Nat

149 | union_ : SnocList Nat -> NSet -> NSet -> NSet

150 | union_ sx l@(x::xs) r@(y::ys) =

151 |   case compare x y of

152 |     LT => union_ (sx:<x) xs r

153 |     GT => union_ (sx:<y) l  ys

154 |     EQ => union_ (sx:<x) xs ys

155 | union_ sx [] ys = sx <>> ys

156 | union_ sx xs [] = sx <>> xs

158 | export %inline

159 | sunion : NSet -> NSet -> NSet

160 | sunion = union_ [<]

167 | public export

168 | record Edge where

169 |   constructor E

170 |   ||| The characters that triggers thi conversion

171 |   rule : Range8

173 |   ||| The target of the given rule

174 |   tgt  : Nat

177 | transitions : Edge -> List (Bits8,Nat)

178 | transitions (E rule tgt) =

179 |   let l := lowerBound rule

180 |       u := upperBound rule

181 |    in case compare l u of

182 |         LT => (,tgt) <$> [l..u]

183 |         EQ => [(l,tgt)]

184 |         GT => []

186 | %runElab derive "Edge" [Show,Eq]

189 | public export

190 | 0 Edges : Type

191 | Edges = List Edge

193 | public export

194 | record ENode where

195 |   constructor EN

196 |   acc : List Nat

197 |   eps : List Nat

198 |   out : Edges

200 | %runElab deriveIndexed "ENode" [Show]

202 | public export

203 | 0 EGraph : Type -> Type

204 | EGraph s = NatMap1 s ENode

208 | public export

209 | record NEdge where

210 |   constructor NE

211 |   ||| The characters that trigger this conversion

212 |   rule : Range8

214 |   ||| The list of targets of the given rule

215 |   tgts : NSet

217 | %runElab derive "NEdge" [Show,Eq]

220 | public export

221 | 0 NEdges : Type

222 | NEdges = List NEdge

224 | public export

225 | record NNode where

226 |   constructor NN

227 |   pos : Nat

228 |   acc : List Nat

229 |   out : NEdges

231 | %runElab deriveIndexed "NNode" [Show]

234 | nchildren : NNode -> List Nat

235 | nchildren (NN _ _ out) = out >>= tgts

237 | public export

238 | 0 NGraph : Type -> Type

239 | NGraph s = NatMap1 s NNode

241 | public export

242 | record Node where

243 |   constructor N

244 |   pos : Nat

245 |   acc : List Nat

246 |   out : Edges

248 | %runElab deriveIndexed "Node" [Show]

251 | children : Node -> List Nat

252 | children n = tgt <$> n.out

254 | public export

255 | 0 Graph : Type -> Type

256 | Graph s = NatMap1 s Node

262 | public export

263 | record DFAState (s,a : Type) where

264 |   [noHints, search s]

265 |   constructor ST

266 |   accs   : NatMap1 s a

267 |   sets   : Ref s (SortedMap NSet Nat)

268 |   egraph : EGraph s

269 |   ngraph : NGraph s

270 |   graph  : Graph s

271 |   cur    : Ref s Nat

274 | init : F1 s (DFAState s a)

275 | init = T1.do

276 |   as <- Types.empty

277 |   ss <- ref1 SortedMap.empty

278 |   eg <- Types.empty

279 |   ng <- Types.empty

280 |   g  <- Types.empty

281 |   cr <- ref1 (S Z)

282 |   pure (ST as ss eg ng g cr)

284 | parameters {auto st : DFAState s a}

286 |   export

287 |   inc : F1 s Nat

288 |   inc = T1.do

289 |     n <- read1 st.cur

290 |     write1 st.cur (S n)

291 |     pure n

293 |   export

294 |   addSet : NSet -> F1 s Nat

295 |   addSet set = T1.do

296 |     n <- inc

297 |     mod1 st.sets (insert set n)

298 |     pure n

300 |   export

301 |   lookupSet : NSet -> F1 s (Maybe Nat)

302 |   lookupSet set = read1 st.sets >>= pure . lookup set

304 |   export %inline

305 |   insertENode : Nat -> ENode -> F1 s Nat

306 |   insertENode k n = insert1 k n st.egraph >> pure k

308 |   export

309 |   insertTerminal : (Nat,t,a) -> F1' s

310 |   insertTerminal (k,_,c) = T1.do

311 |     _ <- insertENode k (EN [k] [] [])

312 |     insert1 k c st.accs

314 |   export %inline

315 |   createENode : ENode -> F1 s Nat

316 |   createENode n = inc >>= (`insertENode` n)

318 |   export %inline

319 |   lookupENode : Nat -> F1 s (Maybe ENode)

320 |   lookupENode n = lookup1 n st.egraph

322 |   export %inline

323 |   getENode : Nat -> F1 s ENode

324 |   getENode n = lookupDflt1 n (EN [] [] []) st.egraph

326 |   export %inline

327 |   insertNNode : Nat -> NNode -> F1' s

328 |   insertNNode k n = insert1 k n st.ngraph

330 |   export %inline

331 |   lookupNNode : Nat -> F1 s (Maybe NNode)

332 |   lookupNNode n = lookup1 n st.ngraph

334 |   export %inline

335 |   getNNode : Nat -> F1 s NNode

336 |   getNNode n = lookupDflt1 n (NN n [] []) st.ngraph

338 |   export %inline

339 |   insertNode : Nat -> Node -> F1' s

340 |   insertNode k n = insert1 k n st.graph

342 |   export %inline

343 |   lookupNode : Nat -> F1 s (Maybe Node)

344 |   lookupNode n = lookup1 n st.graph

346 |   export %inline

347 |   getNode : Nat -> F1 s Node

348 |   getNode n = lookupDflt1 n (N n [] []) st.graph

350 |   export %inline

351 |   evalST : (forall s . DFAState s a => F1 s b) -> b

352 |   evalST f = run1 $ init >>= \st => f @{st}

354 |   export

355 |   normalizeGraph : F1' s

356 |   normalizeGraph = T1.do

357 |     ps  <- pairs1 st.graph

358 |     mp  <- fromList1 (map swap $ zipWithIndex $ map fst ps)

359 |     ps2 <- traverse1 (translate mp) ps

360 |     rs  <- fromList1 ps2

361 |     arr <- read1 rs.ref

362 |     write1 st.graph.ref arr

364 |     where

365 |      translate : NatMap1 s Nat -> (Nat,Node) -> F1 s (Nat,Node)

366 |      translate m (x, N pos acc out) = T1.do

367 |        x2   <- lookupDflt1 x 0 m

368 |        out2 <- traverse1 (\(E r t) => E r <$> lookupDflt1 t 0 m) out

369 |        pure (x2, N x2 acc out2)

375 | public export

376 | record Machine a b where

377 |   constructor M

378 |   terminals : SortedMap Nat a

379 |   graph     : b

384 | machine : (forall s . DFAState s a => F1 s b) -> Machine a b

385 | machine f =

386 |    run1 $ T1.do

387 |      st  <- init

388 |      res <- f @{st}

389 |      ps  <- pairs1 st.accs

390 |      pure (M (SortedMap.fromList ps) res)