0 | module TyRE.Parser

 2 | import Data.Maybe

 4 | import TyRE.Core

 5 | import TyRE.Parser.SM

 6 | import TyRE.Parser.SMConstruction

 7 | import TyRE.DisjointMatches

 9 | %default total

12 | parseFull : (r : TyRE a) -> List Char -> Maybe a

13 | parseFull re cs =

14 |   let _ := compile re

15 |   in runFromInit (runTillStrEnd cs)

18 | parsePrefix : (r : TyRE a) -> List Char -> (greedy : Bool)

19 |             -> (Maybe a, List Char)

20 | parsePrefix re cs False =

21 |   let _ = compile re

22 |   in runFromInit (runTillFirstAccept cs)

23 | parsePrefix re cs True =

24 |   let _ = compile re

25 |   in runFromInit (runTillLastAccept cs Nothing)

28 | partial --we should be able to prove totality thanks to `consuming`

29 | asDisjointMatches : (re : TyRE a) -> {auto 0 consuming : IsConsuming re}

30 |                   -> List Char -> (greedy : Bool)

31 |                   -> DisjointMatches a

32 | asDisjointMatches re cs greedy =

33 |   let _ = compile re

34 |       parseFunction : List Char -> (Maybe a, List Char)

35 |       parseFunction cs =

36 |         if greedy

37 |         then runFromInit (runTillLastAccept cs Nothing)

38 |         else runFromInit (runTillFirstAccept cs)

39 |       matchesRec : List Char -> DisjointMatchesSnoc a

40 |                 -> DisjointMatchesSnoc a 

41 |       matchesRec [] dm = dm

42 |       matchesRec (x :: xs) dm with (parseFunction (x :: xs))

43 |         matchesRec (x :: xs) dm | (Nothing, _) = matchesRec xs (dm :< x)

44 |         matchesRec (x :: xs) dm | ((Just tree), tail) =

45 |           matchesRec tail (dm :+: tree)

46 |   in cast (matchesRec cs (Prefix [<]))

50 | getToken : (r : TyRE a) -> Stream Char -> (greedy : Bool)

51 |         -> (Maybe a, Stream Char)

52 | getToken re cs False =

53 |   let _ = compile re

54 |   in runFromInit (runTillFirstAccept cs)

55 | getToken re cs True =

56 |   let _ = compile re

57 |   in runFromInit (runTillLastAccept cs Nothing)