0 | module Text.Lex.Manual.Syntax
 1 |
 2 | import Text.Lex.Manual
 3 |
 4 | %default total
 5 |
 6 | namespace Tok
 7 |   public export
 8 |   pure : a -> Tok False e a
 9 |   pure v cs = Succ v cs
10 |
11 |   public export
12 |   (>>=) : Tok b1 e a -> (a -> Tok b2 e b) -> Tok (b1 || b2) e b
13 |   (>>=) f g cs =
14 |     let Succ x cs1 @{q} := f cs    | Fail x y z => Fail x y z
15 |      in swapOr $ trans (g x cs1) q
16 |
17 |   public export
18 |   (>>) : Tok b1 e () -> Tok b2 e a -> Tok (b1 || b2) e a
19 |   (>>) f g cs =
20 |     let Succ _ cs1 @{q} := f cs | Fail x y z => Fail x y z
21 |      in swapOr $ trans (g cs1) q
22 |
23 |   public export
24 |   (*>) : Tok b1 e a -> Tok b2 e b -> Tok (b1 || b2) e b
25 |   (*>) f g cs =
26 |     let Succ _ cs1 @{q} := f cs | Fail x y z => Fail x y z
27 |      in swapOr $ trans (g cs1) q
28 |
29 |   public export
30 |   (<*) : Tok b1 e a -> Tok b2 e b -> Tok (b1 || b2) e a
31 |   (<*) f g cs =
32 |     let Succ v cs1 @{q1} := f cs  | Fail x y z => Fail x y z
33 |         Succ _ cs2 @{q2} := g cs1 | Fail x y z => Fail (weaken $ trans x q1) y z
34 |      in Succ v cs2 @{swapOr $ trans q2 q1}
35 |
36 |   public export
37 |   (<*>) : Tok b1 e (a -> b) -> Tok b2 e a -> Tok (b1 || b2) e b
38 |   (<*>) t1 t2 cs =
39 |     let Succ fun cs1 @{q} := t1 cs  | Fail x y z => Fail x y z
40 |         Succ val cs2 @{r} := t2 cs1 | Fail r y z => Fail (weaken $ trans r q) y z
41 |      in Succ (fun val) cs2 @{swapOr $ trans r q}
42 |
43 | namespace AutoTok
44 |
45 |   public export
46 |   pure : a -> AutoTok e a
47 |   pure v cs = Succ v cs
48 |
49 |   public export
50 |   (<*>) : AutoTok e (a -> b) -> AutoTok e a -> AutoTok e b
51 |   (<*>) t1 t2 cs =
52 |     let Succ fun cs1 := t1 cs  | Fail x y z => Fail x y z
53 |         Succ val cs2 := t2 cs1 | Fail x y z => Fail x y z
54 |      in Succ (fun val) cs2
55 |
56 |   public export
57 |   (<*) : AutoTok e a -> AutoTok e b -> AutoTok e a
58 |   (<*) t1 t2 cs =
59 |     let Succ val cs1 := t1 cs  | Fail x y z => Fail x y z
60 |         Succ _   cs2 := t2 cs1 | Fail x y z => Fail x y z
61 |      in Succ val cs2
62 |
63 |   public export
64 |   (>>=) : AutoTok e a -> (a -> AutoTok e b) -> AutoTok e b
65 |   (>>=) f g cs =
66 |     let Succ x cs1 := f cs | Fail x y z => Fail x y z
67 |      in g x cs1
68 |
69 |   public export
70 |   (>>) : AutoTok e () -> AutoTok e a -> AutoTok e a
71 |   (>>) f g cs =
72 |     let Succ _ cs1 := f cs | Fail x y z => Fail x y z
73 |      in g cs1
74 |
75 |   public export
76 |   (*>) : AutoTok e a -> AutoTok e b -> AutoTok e b
77 |   (*>) f g cs =
78 |     let Succ _ cs1 := f cs | Fail x y z => Fail x y z
79 |      in g cs1
80 |