1structure smpp :> smpp =
2struct
3
4infix >- >>
5
6type ('a,'b) t =
7     'a * HOLPP.pretty list -> ('b * ('a * HOLPP.pretty list)) option
8
9open HOLPP
10
11fun consP p (st,ps) = SOME ((), (st, p::ps))
12fun add_string s = consP (HOLPP.PrettyStringWithWidth(s, UTF8.size s))
13fun add_break b = consP (HOLPP.add_break b)
14fun add_stringsz p = consP (HOLPP.PrettyStringWithWidth p)
15fun add_newline x = consP HOLPP.NL x
16fun nothing stps = SOME ((),stps)
17fun fail aps = NONE
18
19fun op>>(p1, p2) stps =
20  case p1 stps of
21      SOME (_, stps1) => p2 stps1
22    | NONE => NONE
23
24fun op>- (p1, fp2) aps =
25  case p1 aps of
26      SOME (b, stps1) => fp2 b stps1
27    | NONE => NONE
28
29fun op|| (p1,p2) apps =
30    case p1 apps of
31      NONE => p2 apps
32    | x => x
33
34fun op||| (p1,fps) apps =
35    case p1 apps of
36      NONE => fps()apps
37    | x => x
38
39fun return x y = SOME (x,y)
40
41fun bs2b bs = bs = HOLPP.CONSISTENT
42
43fun block bs i p (a,ps) =
44  case p (a,[]) of
45      NONE => NONE
46    | SOME(res, (a1,ps1)) =>
47        SOME(res, (a1, PrettyBlock(i, bs2b bs, [], List.rev ps1) :: ps))
48
49fun fupdate f (a,pps) = SOME (a, (f a, pps))
50
51infix >>
52
53fun mapp f [] = nothing
54  | mapp f (e::es) = f e >> mapp f es
55
56fun mmap f [] = return []
57  | mmap f (e::es) = f e >- (fn h => mmap f es >- (fn t => return (h::t)))
58
59fun pr_list fpp brk list =
60    case list of
61      [] => nothing
62    | [b] => fpp b
63    | b::bs => fpp b >> brk >> pr_list fpp brk bs
64
65fun cons x xs = x::xs
66
67fun mappr_list fpp brk list =
68    case list of
69      [] => return []
70    | [b] => fpp b >- (fn bres => return [bres])
71    | b::bs => let
72        fun afterb bres = brk >> mappr_list fpp brk bs >- return o cons bres
73      in
74        fpp b >- afterb
75      end
76
77fun lift pf x =
78  let val pty = pf x in (fn (st,pps) => SOME ((), (st, pty :: pps))) end
79fun lower m st0 =
80  let
81    fun mapthis (a, (st,ps)) = (HOLPP.block CONSISTENT 0 (List.rev ps), a, st)
82  in
83    Option.map mapthis (m (st0, []))
84  end
85
86end (* struct *)
87