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