0 | module TyRE.Parser.SM

  2 | import Data.SnocList

  4 | import Data.Maybe

  5 | import Data.List

  6 | import Data.List.Elem

  7 | import Data.Void

  8 | import Data.DPair

 10 | import TyRE.Extra.Reflects

 12 | %default total

 16 | public export

 17 | data Instruction : SnocList Type -> SnocList Type -> Type where

 18 |   ||| Pushes chosen symbol on the stack

 19 |   Push : {0 x : Type} -> x -> Instruction tps (tps :< x)

 20 |   ||| Pushes currently consumed character on the stack

 21 |   PushChar : Instruction tps (tps :< Char)

 22 |   ||| Reduces two last symbols from the stack accoring to the given funciton

 23 |   ReducePair : {0 x,y,z : Type} -> (x -> y -> z)

 24 |             -> Instruction (tps :< x :< y) (tps :< z)

 25 |   ||| Maps the top element of stack

 26 |   Transform : {0 x,y : Type} -> (x -> y) -> Instruction (tps :< x) (tps :< y)

 27 |   ||| Pushes collected string on the stack

 28 |   EmitString : Instruction tps (tps :< String)

 29 |   ||| Raises record flag and starts collecting characters

 30 |   Record : Instruction tps tps

 32 | public export

 33 | liftInst : Instruction tps tps' -> Instruction (pcds ++ tps) (pcds ++ tps')

 34 | liftInst (Push x) = Push x

 35 | liftInst PushChar = PushChar

 36 | liftInst (ReducePair f) = ReducePair f

 37 | liftInst (Transform f) = Transform f

 38 | liftInst EmitString = EmitString

 39 | liftInst Record = Record

 41 | public export

 42 | data RoutineSnoc : SnocList Type -> SnocList Type -> Type where

 43 |   ||| Identity

 44 |   Lin : RoutineSnoc tps tps

 45 |   ||| Sequences routines

 46 |   (:<) : RoutineSnoc tps tps' -> Instruction tps' tps'' -> RoutineSnoc tps tps''

 48 | public export

 49 | data Routine : SnocList Type -> SnocList Type -> Type where

 50 |   ||| Identity

 51 |   Nil : Routine tps tps

 52 |   ||| Sequences routines

 53 |   (::) : Instruction tps tps' -> Routine tps' tps'' -> Routine tps tps''

 55 | public export

 56 | (++) : RoutineSnoc tps tps' -> RoutineSnoc tps' tps'' -> RoutineSnoc tps tps''

 57 | (++) r [<] = r

 58 | (++) r (x :< y) = (r ++ x) :< y

 60 | public export

 61 | lift : RoutineSnoc tps tps' -> RoutineSnoc (pcds ++ tps) (pcds ++ tps')

 62 | lift [<] = [<]

 63 | lift (x :< y) = (lift x) :< liftInst y

 65 | reverseRec : RoutineSnoc ts ts' -> Routine ts' ts'' -> Routine ts ts''

 66 | reverseRec [<] y = y

 67 | reverseRec (x :< z) y = reverseRec x (z :: y)

 69 | reverse : RoutineSnoc tps tps' -> Routine tps tps'

 70 | reverse sx = reverseRec sx []

 73 | public export

 74 | data EitherErased : Type -> Type -> Type where

 75 |   Left : a -> EitherErased a b

 76 |   Right : (0 y : b) -> EitherErased a b

 78 | namespace IsInit

 79 |   public export

 80 |   data IsInitInstruction : Instruction t t' -> Type where

 81 |     InitRecord : IsInitInstruction Record

 82 |     InitPush : forall elem. IsInitInstruction (Push elem)

 83 |     InitReducePair : IsInitInstruction (ReducePair f)

 84 |     InitTransform : IsInitInstruction (Transform f)

 85 |     InitEmitString : IsInitInstruction EmitString

 87 |   public export

 88 |   data IsInitRoutine : Routine t t' -> Type where

 89 |     Nil  : IsInitRoutine []

 90 |     (::) : IsInitInstruction x -> IsInitRoutine xs -> IsInitRoutine (x :: xs)

 92 |   -- We need explicit projections due to Idris bugs involving irrefutable

 93 |   -- arguments at quantity zero, e.g.:

 94 |   --   https://github.com/idris-lang/Idris2/issues/2513

 95 |   -- Since these pend the new-core rewrite, we use explicit projections to

 96 |   -- work around these issues.

 98 |   public export

 99 |   head : IsInitRoutine (x :: xs) -> IsInitInstruction x

100 |   head (prf :: _) = prf

102 |   public export

103 |   tail : IsInitRoutine (x :: xs) -> IsInitRoutine xs

104 |   tail (_ :: prfs) = prfs

106 |   public export

107 |   data IsInitRoutineSnoc : RoutineSnoc t t' -> Type where

108 |     Lin  : IsInitRoutineSnoc [<]

109 |     (:<) : IsInitRoutineSnoc xs -> IsInitInstruction x

110 |         -> IsInitRoutineSnoc (xs :< x)

112 |   public export

113 |   (++) : IsInitRoutineSnoc xs -> IsInitRoutineSnoc xs'

114 |       -> IsInitRoutineSnoc (xs ++ xs')

115 |   (++) x [<] = x

116 |   (++) x (y :< z) = (x ++ y) :< z

118 |   reverseRec : IsInitRoutineSnoc sx -> IsInitRoutine xs

119 |             -> IsInitRoutine (reverseRec sx xs)

120 |   reverseRec [<] y = y

121 |   reverseRec (x :< z) y = reverseRec x (z :: y)

123 |   export

124 |   reverse : IsInitRoutineSnoc sx -> IsInitRoutine (reverse sx)

125 |   reverse sx = reverseRec sx []

127 |   liftInst : IsInitInstruction xs -> IsInitInstruction (liftInst xs)

128 |   liftInst InitRecord = InitRecord

129 |   liftInst InitPush = InitPush

130 |   liftInst InitReducePair = InitReducePair

131 |   liftInst InitTransform = InitTransform

132 |   liftInst InitEmitString = InitEmitString

134 |   public export

135 |   lift : IsInitRoutineSnoc xs -> IsInitRoutineSnoc (lift xs)

136 |   lift [<] = [<]

137 |   lift (x :< y) = (lift x) :< (liftInst y)

139 | public export

140 | mlookup : (s -> SnocList Type) -> Type -> Maybe s -> SnocList Type

141 | mlookup f t Nothing = [< t]

142 | mlookup f t (Just s) = f s

144 | public export

145 | InitStatesType : (shape : Type) -> (state : Type) -> (stateShape : state -> SnocList Type) -> Type

146 | InitStatesType shape state stateShape =

147 |   List (st : Maybe state

148 |         ** Subset (RoutineSnoc [<] (mlookup stateShape shape st))

149 |                   IsInitRoutineSnoc)

151 | public export

152 | TransitionRelation : (shape : Type) -> (state : Type) -> (stateShape : state -> SnocList Type) -> Type

153 | TransitionRelation shape state stateShape =

154 |     (st : state)

155 |   -> Char

156 |   -> List (st' : Maybe state

157 |             ** RoutineSnoc (stateShape st) (mlookup stateShape shape st'))

159 | public export

160 | record SM (t : Type) where

161 |   constructor MkSM

162 |   0 s : Type

163 |   0 lookup : s -> SnocList Type

164 |   {auto isEq : Eq s}

165 |   init : InitStatesType t s lookup

166 |   next : TransitionRelation t s lookup

169 | namespace Stack

170 |   public export

171 |   data Stack : SnocList Type -> Type where

172 |     Lin : Stack [<]

173 |     (:<) : Stack tps -> {0 t : Type} -> t -> Stack (tps :< t)

175 | record ThreadData (code : SnocList Type) where

176 |   constructor MkThreadData

177 |   stack : Stack code

178 |   recorded : SnocList Char

179 |   rec : Bool

181 | record Thread {t : Type} (sm : SM t) where

182 |   constructor MkThread

183 |   state : Maybe sm.s

184 |   tddata : ThreadData (mlookup sm.lookup t state)

186 | execInstructionAux : {0 scs, scs', p : SnocList Type}

187 |                   -> (r : Instruction scs scs')

188 |                   -> EitherErased Char (IsInitInstruction r)

189 |                   -> ThreadData (p ++ scs)

190 |                   -> ThreadData (p ++ scs')

191 | execInstructionAux Record c (MkThreadData st col rec) =

192 |   MkThreadData st col True

193 | execInstructionAux (Push elem) c (MkThreadData st col rec) =

194 |   MkThreadData (st :< elem) col rec

195 | execInstructionAux PushChar (Left c) (MkThreadData st col rec) =

196 |   MkThreadData (st :< c) col rec

197 | execInstructionAux (ReducePair f) c (MkThreadData (x :< z :< y) col rec) =

198 |   MkThreadData (x :< (f z y)) col rec

199 | execInstructionAux (Transform f) c (MkThreadData (y :< z) col rec) =

200 |   MkThreadData (y :< (f z)) col rec

201 | execInstructionAux EmitString c (MkThreadData st col rec) =

202 |   MkThreadData (st :< (fastPack $ cast col)) [<] False

204 | execRoutineAux : {0 scs, scs', p : SnocList Type}

205 |             -> (r : Routine scs scs')

206 |             -> EitherErased Char (IsInitRoutine r)

207 |             -> ThreadData (p ++ scs)

208 |             -> ThreadData (p ++ scs')

209 | execRoutineAux [] c st = st

210 | execRoutineAux (i :: r) (Left c) st =

211 |   execRoutineAux r (Left c) (execInstructionAux i (Left c) st)

212 | execRoutineAux (i :: r) (Right ipir) st =

213 |   execRoutineAux r (Right $ tail ipir) (execInstructionAux i (Right $ head ipir) st)

215 | execRoutine : {0 scs, scs' : SnocList Type}

216 |             -> (r : Routine scs scs')

217 |             -> EitherErased Char (IsInitRoutine r)

218 |             -> ThreadData scs -> ThreadData scs'

219 | execRoutine r c st =

220 |   rewrite (sym $ appendLinLeftNeutral scs') in

221 |     execRoutineAux {p = [<]} r c (rewrite (appendLinLeftNeutral scs) in st)

223 | execOnThread : (sm : SM c) -> (c : Char) -> Thread sm -> List (Thread sm)

224 | execOnThread sm c (MkThread Nothing info) = []

225 | execOnThread sm c (MkThread (Just st) info) =

226 |   let infoWithChar =

227 |         case info of

228 |           (MkThreadData stack recorded True) =>

229 |             MkThreadData stack (recorded :< c) True

230 |           info => info

231 |   in map (\case (ns ** rt) => MkThread ns (execRoutine (reverse rt) (Left c) infoWithChar))

232 |          (sm.next st c)

234 | getFromStack : Stack [< t] -> t

235 | getFromStack ([< r]) = r

237 | parameters {0 t : Type} {auto sm : SM t}

238 |   ||| Distinct function for threads

239 |   distinct : List (Thread sm) -> List (Thread sm)

240 |   distinct tds = distinctRep tds [] where

241 |     distinctRep : List (Thread sm) -> List (Thread sm) -> List (Thread sm)

242 |     distinctRep [] acc = acc

243 |     distinctRep (td :: tds) acc =

244 |       let _ := sm.isEq

245 |       in case find (\t => t.state == td.state) acc of

246 |           (Just _) => distinctRep tds acc

247 |           Nothing  => distinctRep tds (td :: acc)

248 |   ||| Initial list of threads

249 |   init : List (Thread sm)

250 |   init =

251 |     map (\case

252 |             (st ** (rt `Element` p)) =>

253 |               MkThread st

254 |                       (execRoutine (reverse rt) (Right $ reverse p) (MkThreadData [<] [<] False)))

255 |                       sm.init

257 |   namespace StringRunners -- possible modes of running for list of characters

258 |     ||| Run the state machine matching the whole string

259 |     export

260 |     runTillStrEnd : List Char -> List (Thread sm) -> Maybe t

261 |     runTillStrEnd [] tds with (findR (\td => isNothing (td.state)) tds)

262 |       runTillStrEnd [] tds | (Because Nothing p) = Nothing

263 |       runTillStrEnd [] tds

264 |         | (Because (Just (MkThread Nothing (MkThreadData stack _ _))) _)

265 |         = Just (getFromStack stack)

266 |       runTillStrEnd [] tds

267 |         | (Because (Just (MkThread (Just x) tddata)) (Indeed prf))

268 |         = absurdity {t = Void} (case prf of (y, z) impossible)

269 |     runTillStrEnd (c :: cs) tds =

270 |       runTillStrEnd cs (distinct $ tds >>= (execOnThread sm c))

271 |     ||| Run the state machine looking for a first matching prefix (non-greedy)

272 |     export

273 |     runTillFirstAccept : List Char -> List (Thread sm)

274 |                       -> (Maybe t, List Char)

275 |     runTillFirstAccept cs [] = (Nothing, cs)

276 |     runTillFirstAccept cs tds with (findR (\td => isNothing (td.state)) tds)

277 |       runTillFirstAccept [] tds        | (Because Nothing p) = (Nothing, [])

278 |       runTillFirstAccept (x :: xs) tds | (Because Nothing p) =

279 |         runTillFirstAccept xs (distinct $ tds >>= (execOnThread sm x))

280 |       runTillFirstAccept cs tds

281 |         | (Because (Just (MkThread Nothing (MkThreadData stack _ _))) _)

282 |         = (Just (getFromStack stack), cs)

283 |       runTillFirstAccept cs tds

284 |         | (Because (Just (MkThread (Just x) tddata)) (Indeed prf))

285 |         = absurdity {t = Void} (case prf of (y, z) impossible)

286 |     ||| Run the state machine looking for the last matching prefix (greedy)

287 |     export

288 |     runTillLastAccept : List Char -> Maybe (t, List Char)

289 |                       -> List (Thread sm)

290 |                       -> (Maybe t, List Char)

291 |     runTillLastAccept cs Nothing [] = (Nothing, cs)

292 |     runTillLastAccept cs (Just (tree, rest)) [] = (Just tree, rest)

293 |     runTillLastAccept cs mr tds with (findR (\td => isNothing (td.state)) tds)

294 |       runTillLastAccept [] Nothing tds | (Because Nothing p) =(Nothing, [])

295 |       runTillLastAccept [] (Just (tree, tail)) tds

296 |                         | (Because Nothing p) = (Just tree, tail)

297 |       runTillLastAccept (x :: xs) mr tds | (Because Nothing p) =

298 |         runTillLastAccept xs mr (distinct $ tds >>= (execOnThread sm x))

299 |       runTillLastAccept [] mr tds

300 |         | (Because (Just (MkThread Nothing (MkThreadData stack _ _))) _)

301 |         = (Just (getFromStack stack), [])

302 |       runTillLastAccept (x :: xs) mr tds

303 |         | (Because (Just (MkThread Nothing (MkThreadData stack _ _))) _)

304 |         = runTillLastAccept xs

305 |                             (Just (getFromStack stack, x :: xs))

306 |                             (distinct $ tds >>= (execOnThread sm x))

307 |       runTillLastAccept cs mr tds

308 |         | (Because (Just (MkThread (Just x) tddata)) (Indeed prf))

309 |         = absurdity {t = Void} (case prf of (y, z) impossible)

311 |   namespace StreamRunners -- possible modes of running for streams

312 |     ||| Run the state machine looking for a first matching prefix (non-greedy)

314 |     export

315 |     partial

316 |     runTillFirstAccept : Stream Char -> List (Thread sm)

317 |                       -> (Maybe t, Stream Char)

318 |     runTillFirstAccept cs [] = (Nothing, cs)

319 |     runTillFirstAccept cs tds with (findR (\td => isNothing (td.state)) tds)

320 |       runTillFirstAccept (x :: xs) tds | (Because Nothing p) =

321 |         runTillFirstAccept xs (distinct $ tds >>= (execOnThread sm x))

322 |       runTillFirstAccept cs tds

323 |         | (Because (Just (MkThread Nothing (MkThreadData stack _ _))) _)

324 |         = (Just (getFromStack stack), cs)

325 |       runTillFirstAccept cs tds

326 |         | (Because (Just (MkThread (Just x) tddata)) (Indeed prf))

327 |         = absurdity {t = Void} (case prf of (y, z) impossible)

328 |     ||| Run the state machine looking for the last matching prefix (greedy)

329 |     export

330 |     partial

331 |     runTillLastAccept : Stream Char -> Maybe (t, Stream Char)

332 |                       -> List (Thread sm)

333 |                       -> (Maybe t, Stream Char)

334 |     runTillLastAccept cs Nothing [] = (Nothing, cs)

335 |     runTillLastAccept cs (Just (tree, rest)) [] = (Just tree, rest)

336 |     runTillLastAccept cs mr tds with (findR (\td => isNothing (td.state)) tds)

337 |       runTillLastAccept (x :: xs) mr tds | (Because Nothing p) =

338 |         runTillLastAccept xs mr (distinct $ tds >>= (execOnThread sm x))

339 |       runTillLastAccept (x :: xs) mr tds

340 |         | (Because (Just (MkThread Nothing (MkThreadData stack _ _))) _)

341 |         = runTillLastAccept xs

342 |                             (Just (getFromStack stack, x :: xs))

343 |                             (distinct $ tds >>= (execOnThread sm x))

344 |       runTillLastAccept cs mr tds

345 |         | (Because (Just (MkThread (Just x) tddata)) (Indeed prf))

346 |         = absurdity {t = Void} (case prf of (y, z) impossible)

348 |   export

349 |   runFromInit : (runFunction : List (Thread sm) -> a) -> a

350 |   runFromInit runFunction = runFunction init