1structure wordspp :> wordspp = 2struct 3 4open HolKernel term_pp_types term_pp_utils Hol_pp 5open fcpLib fcpSyntax 6 7val ERR = mk_HOL_ERR "wordsLib" 8 9val word_pp_mode = ref 0 10val word_cast_on = ref false 11val int_word_pp = ref false 12 13val _ = Feedback.register_btrace ("word cast printing", word_cast_on) 14val _ = Feedback.register_trace ("word printing", word_pp_mode, 6) 15val _ = Feedback.register_btrace ("word pp as 2's comp", int_word_pp) 16 17local 18 fun lsr (x, y) = 19 if x = Arbnum.zero orelse y = Arbnum.zero 20 then x 21 else lsr (Arbnum.div2 x, Arbnum.less1 y) 22 fun int_word (v, m) = 23 if !int_word_pp andalso m <> Arbnum.zero 24 then let 25 val top = lsr (v, Arbnum.less1 m) 26 val neg = top = Arbnum.one 27 val nv = 28 if neg then Arbnum.- (Arbnum.pow (Arbnum.two, m), v) else v 29 in 30 (neg, nv) 31 end 32 else (false, v) 33 val hexsplit = Arbnum.fromHexString "10000" 34 fun f (l, v) = 35 if !word_pp_mode = 0 andalso Arbnum.<= (hexsplit, v) 36 then "0x" ^ Arbnum.toHexString v 37 else if !word_pp_mode = 0 orelse !word_pp_mode = 3 38 then Arbnum.toString v 39 else if !word_pp_mode = 1 40 then "0b" ^ Arbnum.toBinString v 41 else if !word_pp_mode = 2 42 then if !base_tokens.allow_octal_input 43 orelse Arbnum.< (v, Arbnum.fromInt 8) 44 then "0" ^ Arbnum.toOctString v 45 else ( Feedback.HOL_MESG 46 "Octal output is only supported when \ 47 \base_tokens.allow_octal_input is true." 48 ; Arbnum.toString v 49 ) 50 else if !word_pp_mode = 6 andalso l mod 4 = 0 51 then "0x" ^ StringCvt.padLeft #"0" (l div 4) (Arbnum.toHexString v) 52 else if !word_pp_mode = 4 orelse !word_pp_mode = 6 53 then "0x" ^ Arbnum.toHexString v 54 else if !word_pp_mode = 5 55 then "0b" ^ StringCvt.padLeft #"0" l (Arbnum.toBinString v) 56 else raise ERR "output_words_as" "invalid printing mode" 57 fun dest_word_type ty = 58 let 59 val (a, b) = fcpSyntax.dest_cart_type ty 60 val _ = a = Type.bool orelse 61 raise ERR "dest_word_type" "not an instance of :bool['a]" 62 in 63 b 64 end 65 val dim_of = dest_word_type o Term.type_of 66in 67 fun words_printer Gs backend sys ppfns gravs d t = 68 let 69 open Portable term_pp_types smpp 70 infix >> 71 val {add_string=str, add_break=brk,...} = 72 ppfns: term_pp_types.ppstream_funs 73 val x = dim_of t 74 val (_, n) = dest_comb t 75 val m = fcpLib.index_to_num x handle HOL_ERR _ => Arbnum.zero 76 val v = numSyntax.dest_numeral n 77 val (neg, v) = int_word (v, m) 78 in 79 (if !Globals.show_types orelse !word_cast_on 80 then str "(" 81 else nothing) 82 >> (if neg then str "-" else nothing) 83 >> str (f (Arbnum.toInt m, v) ^ "w") 84 >> (if !Globals.show_types orelse !word_cast_on 85 then brk (1, 2) 86 >> lift pp_type (type_of t) 87 >> str ")" 88 else nothing) 89 end 90 handle HOL_ERR _ => raise term_pp_types.UserPP_Failed 91end 92 93val _ = term_grammar.userSyntaxFns.register_userPP 94 {name = "wordspp.words_printer", 95 code = words_printer} 96 97(* ------------------------------------------------------------------------- 98 A pretty-printer that shows the types for ><, w2w and @@ 99 ------------------------------------------------------------------------- *) 100 101fun words_cast_printer Gs backend syspr ppfns (pg, lg, rg) d t = 102 let 103 open Portable term_pp_types smpp 104 infix >> 105 val ppfns : ppstream_funs = ppfns 106 val {add_string = str, add_break = brk, ublock,...} = ppfns 107 fun stype tm = String.extract (type_to_string (type_of tm), 1, NONE) 108 fun delim i act = 109 case pg of 110 Prec (j, _) => if i <= j then act else nothing 111 | _ => nothing 112 val (f, x) = strip_comb t 113 fun sys g d t = syspr {gravs = g, depth = d, binderp = false} t 114 in 115 case (dest_thy_const f, x) of 116 ({Name = "n2w", Thy = "words", Ty = ty}, [a]) => 117 let 118 val prec = Prec (2000, "n2w") 119 in 120 ublock INCONSISTENT 0 121 (delim 200 (str "(") 122 >> str "(n2w " 123 >> lift pp_type ty 124 >> str ")" 125 >> brk (1, 2) 126 >> sys (prec, prec, prec) (d - 1) a 127 >> delim 200 (str ")")) 128 end 129 | ({Name = "w2w", Thy = "words", Ty = ty}, [a]) => 130 let 131 val prec = Prec (2000, "w2w") 132 in 133 ublock INCONSISTENT 0 134 (delim 200 (str "(") 135 >> str "(w2w " 136 >> lift pp_type ty 137 >> str ")" 138 >> brk (1, 2) 139 >> sys (prec, prec, prec) (d - 1) a 140 >> delim 200 (str ")")) 141 end 142 | ({Name = "sw2sw", Thy = "words", Ty = ty}, [a]) => 143 let 144 val prec = Prec (2000, "sw2sw") 145 in 146 ublock INCONSISTENT 0 147 (delim 200 (str "(") 148 >> str "(sw2sw " 149 >> lift pp_type ty 150 >> str ")" 151 >> brk (1, 2) 152 >> sys (prec, prec, prec) (d - 1) a 153 >> delim 200 (str ")")) 154 end 155 | ({Name = "word_concat", Thy = "words", Ty = ty}, [a, b]) => 156 let 157 val prec = Prec (2000, "word_concat") 158 in 159 ublock INCONSISTENT 0 160 (delim 200 (str "(") 161 >> str "(word_concat " 162 >> lift pp_type ty 163 >> str ")" 164 >> brk (1, 2) 165 >> sys (prec, prec, prec) (d - 1) a 166 >> brk (1, 0) 167 >> sys (prec, prec, prec) (d - 1) b 168 >> delim 200 (str ")")) 169 end 170 | ({Name = "word_extract", Thy = "words", Ty = ty}, [h, l, a]) => 171 let 172 val prec = Prec (2000, "word_extract") 173 in 174 ublock INCONSISTENT 0 175 (delim 200 (str "(") 176 >> str "(" 177 >> str "(" 178 >> sys (prec, prec, prec) (d - 1) h 179 >> brk (1, 2) 180 >> str "><" 181 >> brk (1, 2) 182 >> sys (prec, prec, prec) (d - 1) l 183 >> str ")" 184 >> brk (1, 2) 185 >> lift pp_type (type_of (list_mk_comb (f, [h, l]))) 186 >> str ")" 187 >> brk (1, 2) 188 >> sys (prec, prec, prec) (d - 1) a 189 >> delim 200 (str ")")) 190 end 191 | _ => raise term_pp_types.UserPP_Failed 192 end 193 handle HOL_ERR _ => raise term_pp_types.UserPP_Failed 194 195val _ = term_grammar.userSyntaxFns.register_userPP 196 {name = "wordspp.words_cast_printer", 197 code = words_cast_printer} 198 199end 200