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 123fun mk_numerallit_term n = 124 let 125 val num_ty = mk_thy_type{Thy = "num", Tyop = "num", Args = []} 126 val ALT_ZERO = 127 mk_thy_const{Thy = "arithmetic", Name = "ZERO", Ty = num_ty} 128 val ZERO = mk_thy_const{Thy = "num", Name = "0", Ty = num_ty} 129 fun mkf s = 130 mk_thy_const{Thy = "arithmetic", Name = s, Ty = num_ty --> num_ty} 131 in 132 gen_mk_numeral{mk_comb=mk_comb,ZERO = ZERO, ALT_ZERO= ALT_ZERO, 133 NUMERAL = mkf "NUMERAL", BIT1 = mkf "BIT1", 134 BIT2 = mkf "BIT2"} n 135 end 136 137(*--------------------------------------------------------------------------- 138 STRINGS 139 ---------------------------------------------------------------------------*) 140 141val dest_chr = sdest_monop ("CHR","string") (ERR "dest_chr" "") 142val dest_string = sdest_binop ("CONS","list") (ERR "dest_string" "") 143val fromHOLchar = Char.chr o Arbnum.toInt o dest_numeral o dest_chr 144 145val dest_char_lit = fromHOLchar 146val is_char_lit = can dest_char_lit 147 148fun is_char_type ty = let 149 val {Thy,Tyop,Args} = dest_thy_type ty 150in 151 Thy = "string" andalso Tyop = "char" andalso null Args 152end handle HOL_ERR _ => false 153 154fun is_string_type ty = let 155 val {Thy,Tyop,Args} = dest_thy_type ty 156in 157 Thy = "list" andalso Tyop = "list" andalso List.all is_char_type Args 158end handle HOL_ERR _ => false 159 160fun is_emptystring tm = 161 case total dest_thy_const tm of 162 SOME {Name="NIL",Thy="list",Ty} => is_string_type Ty 163 | otherwise => false 164 165fun dest_string_lit tm = 166 if is_emptystring tm then "" 167 else let 168 val (front,e) = Lib.front_last (strip_binop dest_string tm) 169 in 170 if is_emptystring e then 171 String.implode (itlist (cons o fromHOLchar) front []) 172 else raise ERR "dest_string_lit" "not terminated by EMPTYSTRING" 173 end 174 175val is_string_lit = can dest_string_lit 176 177val paranoid_stringlitpp = ref false 178val _ = Feedback.register_btrace 179 ("paranoid string literal printing", paranoid_stringlitpp) 180fun string_literalpp {ldelim,rdelim} s = 181 if not (!paranoid_stringlitpp) then 182 ldelim ^ String.toString s ^ rdelim 183 else let 184 val limit = size s 185 fun sub i = String.sub(s,i) 186 fun extract(i,c) = String.extract(s,i,c) 187 val concat = String.concat 188 val toString = String.toString 189 fun recurse A lastc start i = 190 if i >= limit then 191 concat (List.rev(rdelim :: toString (extract(start,NONE))::A)) 192 else 193 case (lastc, sub i) of 194 (#"(", #"*") => let 195 val p = 196 toString (extract(start,SOME (i - start - 1))) ^ "(\\042" 197 in 198 recurse (p::A) #" " (i + 1) (i + 1) 199 end 200 | (#"*", #")") => let 201 val p = 202 toString (extract(start,SOME(i - start - 1))) ^ "\\042)" 203 in 204 recurse (p::A) #" " (i + 1) (i + 1) 205 end 206 | (_, c) => recurse A c start (i + 1) 207 in 208 recurse [ldelim] #" " 0 0 209 end 210 211fun delim_pair {ldelim} = 212 case ldelim of 213 "\"" => {ldelim = "\"", rdelim = "\""} 214 | "\194\171" => {ldelim = ldelim, rdelim = "\194\187"} 215 | "\226\128\185" => {ldelim = ldelim, rdelim = "\226\128\186"} 216 | _ => raise Fail ("delim_pair: bad left delim: "^ldelim) 217 218(*---------------------------------------------------------------------------*) 219(* Redefine dest_string_lit to handle cases where c in CHR (c) is either a *) 220(* "bare" numeral or of the form (NUMERAL ...). Used in ML generation. *) 221(*---------------------------------------------------------------------------*) 222 223local 224 val fromHOLchar = Char.chr o Arbnum.toInt o relaxed_dest_numeral o dest_chr 225in 226fun relaxed_dest_string_lit tm = 227 if is_emptystring tm then "" 228 else let 229 val (front,e) = Lib.front_last (strip_binop dest_string tm) 230 in 231 if is_emptystring e then 232 String.implode (itlist (cons o fromHOLchar) front []) 233 else raise ERR "relaxed_dest_string_lit" 234 "not terminated by EMPTYSTRING" 235 end 236end; 237 238fun mk_string_lit {mk_string,fromMLchar,emptystring} s = let 239 fun recurse (acc, i) = 240 if i < 0 then acc 241 else let 242 val c = String.sub(s,i) 243 in 244 recurse (mk_string (fromMLchar c, acc), i - 1) 245 end 246in 247 recurse (emptystring, String.size s - 1) 248end 249 250fun mk_charlit_term c = 251 let 252 val char_ty = mk_thy_type{Args = [], Thy = "string", Tyop = "char"} 253 val num_ty = mk_thy_type{Args = [], Thy = "num", Tyop = "num"} 254 val CHR_t = 255 mk_thy_const{Name = "CHR", Thy = "string", Ty = num_ty --> char_ty} 256 in 257 c |> Char.ord |> Arbnum.fromInt |> mk_numerallit_term 258 |> curry mk_comb CHR_t 259 end handle HOL_ERR _ => 260 raise ERR "mk_charlit_term" 261 "Can't build character values in this theory context" 262 263fun mk_stringlit_term s = 264 let 265 val char_ty = mk_thy_type{Args = [], Thy = "string", Tyop = "char"} 266 val string_ty = mk_thy_type{Args = [char_ty], Thy = "list", Tyop = "list"} 267 val cons_t = mk_thy_const{Name = "CONS", Thy = "list", 268 Ty = char_ty --> (string_ty --> string_ty)} 269 fun mks (t1, t2) = list_mk_comb(cons_t, [t1,t2]) 270 in 271 mk_string_lit {mk_string = mks, fromMLchar = mk_charlit_term, 272 emptystring = mk_thy_const{Name = "NIL", Thy = "list", 273 Ty = string_ty}} 274 s 275 end handle HOL_ERR _ => 276 raise ERR "mk_stringlit_term" 277 "Can't build string values in this theory context" 278 279 280(*---------------------------------------------------------------------------*) 281(* There are other possible literals, e.g. for word[n]. This ref cell is *) 282(* updated when a new class of literals is created. This is used by the *) 283(* function definition package to help process definitions with literals in *) 284(* patterns. *) 285(*---------------------------------------------------------------------------*) 286 287local 288 val literals = ref [is_numeral, is_string_lit, is_char_lit] 289in 290 fun add_literal is_lit = literals := !literals @ [is_lit] 291 fun is_literal tm = List.exists (fn f => f tm) (!literals) 292end 293 294fun is_pure_literal x = 295 is_literal x andalso not (is_zero x) andalso not (is_string_lit x); 296 297 298end (* Literal *) 299