1(*---------------------------------------------------------------------------*
2 *    Literals for numbers and strings.
3 *
4 * A numeral is a nest of BIT{1,2}s built up from ALT_ZERO wrapped
5 * inside the NUMERAL tag, or it is a straight ZERO constant.  This
6 * difference in treatment between zero and the other numerals leaves
7 * zero as a constant in the logic, which is useful elsewhere.
8 * (Principle of least surprises and all that.)  The use of ALT_ZERO rather
9 * than ZERO inside the representations for other numerals means that
10 * theorems of the form 0 = x will not match inside other numerals.
11 *
12 * A string literal is a bit like a list of characters, except that
13 * CONS is replaced by STRING and NIL is replaced by EMPTYSTRING.
14 *
15 *     STRING (CHAR c_0) (STRING ... (STRING (CHAR c_n) EMPTYSTRING) ...)
16 *
17 * The code in this structure has been generalized to work with
18 * terms and also preterms, since it is also used to build preterms
19 * by the parser.
20 *---------------------------------------------------------------------------*)
21
22structure Literal :> Literal =
23struct
24
25open HolKernel;
26
27type num = Arbnum.num;
28
29val ERR = mk_HOL_ERR "Literal";
30
31(*---------------------------------------------------------------------------
32                 NUMERALS
33 ---------------------------------------------------------------------------*)
34
35fun is_numtype ty =
36   if Type.is_vartype ty then false
37   else case Type.dest_thy_type ty
38         of {Thy="num",Tyop="num", Args=[]} => true
39          | _ => false
40
41fun is_num2num_type ty =
42   let val (ty1,ty2) = Type.dom_rng ty
43   in is_numtype ty1 andalso is_numtype ty2
44   end handle HOL_ERR _ => false;
45
46(*---------------------------------------------------------------------------
47    Checks if t is 0 or a sequence of applications of BIT1 and BIT2 to ZERO,
48    perhaps with an outer application of NUMERAL. In BNF :
49
50     <numeral> ::= 0 | NUMERAL <bits>
51     <bits>    ::= ZERO | BIT1 (<bits>) | BIT2 (<bits>)
52 ---------------------------------------------------------------------------*)
53
54fun dest_zero t =
55 case total dest_thy_const t
56  of SOME {Name="0", Thy="num",...} => Arbnum.zero
57   | otherwise => raise ERR "dest_zero" "expected 0";
58
59fun dest_ZERO t =
60 case total dest_thy_const t
61  of SOME {Name="ZERO", Thy="arithmetic",...} => Arbnum.zero
62   | otherwise => raise ERR "dest_zero" "expected ZERO";
63
64fun dest_b1 tm =
65 case total ((dest_thy_const##I) o dest_comb) tm
66  of SOME ({Name="BIT1", Thy="arithmetic",...},t) => t
67   | otherwise => raise ERR "dest_b1" "expected BIT1";
68
69fun dest_b2 tm =
70 case total ((dest_thy_const##I) o dest_comb) tm
71  of SOME ({Name="BIT2", Thy="arithmetic",...},t) => t
72   | otherwise => raise ERR "dest_b2" "expected BIT2";
73
74local open Arbnum
75in
76fun dest_bare_numeral t =
77  dest_ZERO t
78  handle HOL_ERR _ => two * dest_bare_numeral (dest_b1 t) + one
79  handle HOL_ERR _ => two * dest_bare_numeral (dest_b2 t) + two
80end
81
82fun dest_numeral tm =
83 dest_zero tm
84 handle HOL_ERR _ =>
85    (case total ((dest_thy_const##I) o dest_comb) tm
86      of SOME ({Name="NUMERAL", Thy="arithmetic",...},t)
87         => with_exn dest_bare_numeral t
88              (ERR "dest_numeral" "term is not a numeral")
89       | otherwise => raise ERR "dest_numeral" "term is not a numeral"
90    )
91
92
93(*---------------------------------------------------------------------------
94   A "relaxed" numeral is one where the NUMERAL might not be there. These
95   occasionally occur, for example when the NUMERAL tag has been rewritten
96   away. In BNF :
97
98     <relaxed_numeral> ::= 0 | NUMERAL <bits> | <bits>
99     <bits>            ::= ZERO | BIT1 (<bits>) | BIT2 (<bits>)
100 ---------------------------------------------------------------------------*)
101
102fun relaxed_dest_numeral tm =
103                     dest_numeral tm
104 handle HOL_ERR _ => dest_bare_numeral tm
105 handle HOL_ERR _ => raise ERR "relaxed_dest_numeral" "term is not a numeral";
106
107val is_zero = Lib.can dest_zero;
108val is_ZERO = Lib.can dest_ZERO;
109val is_bare_numeral = Lib.can dest_bare_numeral;
110val is_numeral = Lib.can dest_numeral;
111
112fun gen_mk_numeral {mk_comb, ZERO, ALT_ZERO, NUMERAL, BIT1, BIT2} n =
113 let open Arbnum
114     fun positive x =
115       if x = zero then ALT_ZERO else
116       if x mod two = one
117         then mk_comb(BIT1, positive ((x-one) div two))
118         else mk_comb(BIT2, positive ((x-two) div two))
119 in
120   if n=zero then ZERO else mk_comb(NUMERAL,positive n)
121 end;
122
123
124(*---------------------------------------------------------------------------
125                  STRINGS
126 ---------------------------------------------------------------------------*)
127
128val dest_chr    = sdest_monop ("CHR","string") (ERR "dest_chr" "")
129val dest_string = sdest_binop ("CONS","list") (ERR "dest_string" "")
130val fromHOLchar = Char.chr o Arbnum.toInt o dest_numeral o dest_chr
131
132val dest_char_lit = fromHOLchar
133val is_char_lit = can dest_char_lit
134
135fun is_char_type ty = let
136  val {Thy,Tyop,Args} = dest_thy_type ty
137in
138  Thy = "string" andalso Tyop = "char" andalso null Args
139end handle HOL_ERR _ => false
140
141fun is_string_type ty = let
142  val {Thy,Tyop,Args} = dest_thy_type ty
143in
144  Thy = "list" andalso Tyop = "list" andalso List.all is_char_type Args
145end handle HOL_ERR _ => false
146
147fun is_emptystring tm =
148  case total dest_thy_const tm of
149    SOME {Name="NIL",Thy="list",Ty} => is_string_type Ty
150  | otherwise => false
151
152fun dest_string_lit tm =
153    if is_emptystring tm then ""
154    else let
155        val (front,e) = Lib.front_last (strip_binop (total dest_string) tm)
156      in
157        if is_emptystring e then
158          String.implode (itlist (cons o fromHOLchar) front [])
159        else raise ERR "dest_string_lit" "not terminated by EMPTYSTRING"
160      end
161
162val is_string_lit = can dest_string_lit
163
164val paranoid_stringlitpp = ref false
165val _ = Feedback.register_btrace
166            ("paranoid string literal printing", paranoid_stringlitpp)
167fun string_literalpp s =
168    if not (!paranoid_stringlitpp) then Lib.mlquote s
169    else let
170        val limit = size s
171        fun sub i = String.sub(s,i)
172        fun extract(i,c) = String.extract(s,i,c)
173        val concat = String.concat
174        val toString = String.toString
175        fun recurse A lastc start i =
176            if i >= limit then concat (List.rev("\"" :: extract(start,NONE)::A))
177            else
178              case (lastc, sub i) of
179                (#"(", #"*") => let
180                  val p = toString (extract(start,SOME (i - start - 1))) ^ "(\\042"
181                in
182                  recurse (p::A) #" " (i + 1) (i + 1)
183                end
184              | (#"*", #")") => let
185                  val p = toString (extract(start,SOME(i - start - 1))) ^ "\\042)"
186                in
187                  recurse (p::A) #" " (i + 1) (i + 1)
188                end
189              | (_, c) => recurse A c start (i + 1)
190      in
191        recurse ["\""] #" " 0 0
192      end
193
194
195
196(*---------------------------------------------------------------------------*)
197(* Redefine dest_string_lit to handle cases where c in CHR (c) is either a   *)
198(* "bare" numeral or of the form (NUMERAL ...). Used in ML generation.       *)
199(*---------------------------------------------------------------------------*)
200
201local
202  val fromHOLchar = Char.chr o Arbnum.toInt o relaxed_dest_numeral o dest_chr
203in
204fun relaxed_dest_string_lit tm =
205    if is_emptystring tm then ""
206    else let
207        val (front,e) = Lib.front_last (strip_binop (total dest_string) tm)
208      in
209        if is_emptystring e then
210          String.implode (itlist (cons o fromHOLchar) front [])
211        else raise ERR "relaxed_dest_string_lit"
212                       "not terminated by EMPTYSTRING"
213      end
214end;
215
216fun mk_string_lit {mk_string,fromMLchar,emptystring} s = let
217  fun recurse (acc, i) =
218      if i < 0 then acc
219      else let
220          val c = String.sub(s,i)
221        in
222          recurse (mk_string (fromMLchar c, acc), i - 1)
223        end
224in
225  recurse (emptystring, String.size s - 1)
226end
227
228(*---------------------------------------------------------------------------*)
229(* There are other possible literals, e.g. for word[n]. This ref cell is     *)
230(* updated when a new class of literals is created. This is used by the      *)
231(* function definition package to help process definitions with literals in  *)
232(* patterns.                                                                 *)
233(*---------------------------------------------------------------------------*)
234
235local
236   val literals = ref [is_numeral, is_string_lit, is_char_lit]
237in
238   fun add_literal is_lit = literals := !literals @ [is_lit]
239   fun is_literal tm = List.exists (fn f => f tm) (!literals)
240end
241
242fun is_pure_literal x =
243  is_literal x andalso not (is_zero x) andalso not (is_string_lit x);
244
245
246end (* Literal *)
247