1structure parmonadsyntax :> parmonadsyntax = 2struct 3 4open HolKernel Parse Feedback 5 6local open oneTheory in end 7 8val monadseq_special = "__monad_sequence" 9val monad_emptyseq_special = "__monad_emptyseq" 10val monadassign_special = "__monad_assign" 11val monad_bind = "monad_bind" 12val monad_par = "monad_par" 13 14val par_prec = 90 15val ass_prec = 100 16 17val genvar = "_%" (* impossible to type in as a variable; lexer splits it *) 18fun is_genvar t = #2 (dest_var t) = oneSyntax.one_ty handle HOL_ERR _ => false 19 20val _ = temp_add_listform {block_info = (PP.CONSISTENT,0), 21 cons = monadseq_special, 22 nilstr = monad_emptyseq_special, 23 leftdelim = [TOK "do", BreakSpace(1,2)], 24 rightdelim = [TOK "od"], 25 separator = [TOK ";", BreakSpace(1,0)]} 26 27val _ = temp_add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 28 fixity = Infix(NONASSOC, ass_prec), 29 paren_style = OnlyIfNecessary, 30 pp_elements = [BreakSpace(1,0), TOK "<-", HardSpace 1], 31 term_name = monadassign_special} 32 33val _ = temp_add_rule {block_style = (AroundSameName, (PP.INCONSISTENT, 2)), 34 fixity = Infix(RIGHT, par_prec), 35 paren_style = OnlyIfNecessary, 36 pp_elements = [BreakSpace(1,0), TOK "|||", HardSpace 1], 37 term_name = monad_par} 38 39fun to_vstruct a = let 40 open Absyn 41in 42 case a of 43 AQ x => VAQ x 44 | IDENT x => VIDENT x 45 | QIDENT(loc,_,_) => 46 raise mk_HOL_ERRloc "Absyn" "to_vstruct" loc 47 "Qualified identifiers can't be varstructs" 48 | APP(loc1, APP(loc2, IDENT (loc3, ","), arg1), arg2) => 49 VPAIR(loc1, to_vstruct arg1, to_vstruct arg2) 50 | TYPED (loc, a0, pty) => VTYPED(loc, to_vstruct a0, pty) 51 | _ => raise mk_HOL_ERRloc "Absyn" "to_vstruct" (locn_of_absyn a) 52 "Bad form of varstruct" 53end 54 55fun clean_action a = let 56 open Absyn 57 val unit_pty = Pretype.Tyop{Args = [], Thy = "one", Tyop = "one"} 58 fun mk_bare a = (VTYPED (locn.Loc_None, 59 VIDENT (locn.Loc_None, genvar), 60 unit_pty), 61 a) 62 63in 64 case a of 65 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let 66 in 67 if s = monadassign_special then 68 (to_vstruct arg1, arg2) 69 else if s = monad_par then let 70 val (v1,a1) = clean_action arg1 71 val (v2,a2) = clean_action arg2 72 in 73 (VPAIR(loc1,v1,v2), 74 APP(loc1, APP(loc2, IDENT(loc3, s), a1), a2)) 75 end 76 else mk_bare a 77 end 78 | _ => mk_bare a 79end 80 81fun cleanseq a = let 82 open Absyn 83in 84 case a of 85 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let 86 in 87 if s = monadseq_special then let 88 val (bv, arg1') = clean_action (clean_do true arg1) 89 val arg2' = clean_actions arg2 90 in 91 case arg2' of 92 NONE => SOME arg1' 93 | SOME a => let 94 in 95 SOME (APP(loc1, APP(loc2, 96 IDENT(loc3, monad_bind), 97 arg1'), 98 LAM(locn_of_absyn a, bv, a))) 99 end 100 end 101 else NONE 102 end 103 | _ => NONE 104end 105and clean_do indo a = let 106 open Absyn 107 val clean_do = clean_do indo 108in 109 case cleanseq a of 110 SOME a => a 111 | NONE => let 112 in 113 case a of 114 APP(l,arg1 as APP(_,IDENT(_,s),_),arg2) => 115 if s = monadassign_special andalso not indo then 116 raise mk_HOL_ERRloc "monadsyntax" "clean_do" l 117 "Bare monad assign arrow illegal" 118 else APP(l,clean_do arg1,clean_do arg2) 119 | APP(l,a1,a2) => APP(l,clean_do a1, clean_do a2) 120 | LAM(l,v,a) => LAM(l,v,clean_do a) 121 | IDENT(loc,s) => if s = monad_emptyseq_special then 122 raise mk_HOL_ERRloc "monadsyntax" "clean_do" loc 123 "Empty do-od pair illegal" 124 else a 125 | TYPED(l,a,pty) => TYPED(l,clean_do a,pty) 126 | _ => a 127 end 128end 129and clean_actions a = let 130 open Absyn 131in 132 case cleanseq a of 133 SOME a => SOME a 134 | NONE => let 135 in 136 case a of 137 IDENT(loc,s) => if s = monad_emptyseq_special then NONE 138 else SOME a 139 | a => SOME a 140 end 141end 142 143fun transform_absyn G a = clean_do false a 144 145val _ = Parse.temp_add_absyn_postprocessor ("parmonadsyntax.transform_absyn", 146 transform_absyn) 147 148 149fun dest_binop s G t = let 150 open term_pp_types 151 val oinfo = term_grammar.overload_info G 152 val (fx, y) = dest_comb t 153 val (f, x) = dest_comb fx 154 val prname = case Overload.overloading_of_term oinfo f of 155 NONE => if is_var f then #1 (dest_var f) 156 else raise UserPP_Failed 157 | SOME s => s 158 val _ = prname = s orelse raise UserPP_Failed 159in 160 SOME (x, y) 161end handle HOL_ERR _ => NONE 162 | term_pp_types.UserPP_Failed => NONE 163 164val dest_par = dest_binop monad_par 165val dest_bind = dest_binop monad_bind 166 167fun print_monads (tyg, tmg) backend sysprinter ppfns (p,l,r) depth t = let 168 open smpp term_pp_utils 169 infix >> >- 170 val ppfns = ppfns : term_pp_types.ppstream_funs 171 open term_pp_types term_grammar 172 val (strn,brk) = (#add_string ppfns, #add_break ppfns) 173 val ublock = #ublock ppfns 174 fun pbegin b = if b then strn "(" else nothing 175 fun pend b = if b then strn ")" else nothing 176 val (arg1, arg2) = valOf (dest_bind tmg t) 177 handle Option => raise UserPP_Failed 178 fun syspr bp gravs t = 179 sysprinter {gravs = gravs, depth = depth - 1, binderp = bp} t 180 fun pr_action (p,l,r) (vopt, action) = let 181 fun atomic_assign () = let 182 fun check_grav grav = 183 case grav of 184 Prec(n, _) => n > ass_prec 185 | _ => false 186 val bracketp = check_grav l orelse check_grav r 187 val prec = Prec(ass_prec, monadassign_special) 188 val bvars = free_vars (valOf vopt) 189 in 190 pbegin bracketp >> 191 ublock PP.INCONSISTENT 0 192 (record_bvars bvars (syspr true (prec, l, prec) (valOf vopt)) >> 193 strn " " >> strn "<-" >> brk(1,2) >> 194 syspr false (prec,prec,r) action) >> 195 pend bracketp >> 196 addbvs bvars 197 end 198 in 199 case vopt of 200 NONE => syspr false (p,l,r) action 201 | SOME v => let 202 in 203 case dest_par tmg action of 204 NONE => let 205 in 206 if is_genvar v then syspr false (p,l,r) action 207 else atomic_assign() 208 end 209 | SOME (a1, a2) => let 210 in 211 case Lib.total pairSyntax.dest_pair v of 212 NONE => atomic_assign() 213 | SOME(v1, v2) => let 214 fun check_grav a grav = 215 case grav of 216 Prec(n, _) => n > par_prec orelse (n = par_prec andalso 217 a <> RIGHT) 218 | _ => false 219 val bracketp = check_grav RIGHT l orelse check_grav LEFT r 220 val prec = Prec(par_prec, monad_par) 221 in 222 pbegin bracketp >> 223 ublock PP.CONSISTENT 0 224 (pr_action (prec,l,prec) (SOME v1, a1) >> 225 strn " " >> strn "|||" >> 226 brk(1,0) >> 227 pr_action (prec,prec,r) (SOME v2, a2)) >> 228 pend bracketp 229 end 230 end 231 end 232 end 233 234 fun brk_bind arg1 arg2 = let 235 val (v,body) = (SOME ## I) (pairSyntax.dest_pabs arg2) 236 handle HOL_ERR _ => (NONE, arg2) 237 in 238 ((v, arg1), body) 239 end 240 fun strip acc t = 241 case dest_bind tmg t of 242 NONE => List.rev ((NONE, t) :: acc) 243 | SOME (arg1, arg2) => let 244 val (arg1', arg2') = brk_bind arg1 arg2 245 in 246 strip (arg1'::acc) arg2' 247 end 248 val (arg1',arg2') = brk_bind arg1 arg2 249 val actions = strip [arg1'] arg2' 250in 251 ublock PP.CONSISTENT 0 252 (strn "do" >> brk(1,2) >> 253 getbvs >- (fn oldbvs => 254 pr_list (pr_action(Top,Top,Top)) 255 (strn ";" >> brk(1,2)) 256 actions >> 257 brk(1,0) >> 258 strn "od" >> setbvs oldbvs)) 259end 260 261val _ = temp_add_user_printer ("parmonadsyntax.print_monads", ``x:'a``, 262 print_monads) 263 264val _ = TexTokenMap.temp_TeX_notation {hol = "<-", TeX = ("\\HOLTokenLeftmap{}", 1)} 265val _ = TexTokenMap.temp_TeX_notation {hol = "do", TeX = ("\\HOLKeyword{do}", 2)} 266val _ = TexTokenMap.temp_TeX_notation {hol = "od", TeX = ("\\HOLKeyword{od}", 2)} 267end (* struct *) 268