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