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