1(* Copyright (c) 2009-2011 Tjark Weber. All rights reserved. *) 2 3(* Common auxiliary functions, tracing *) 4 5structure Library = 6struct 7 8 (***************************************************************************) 9 (* tracing *) 10 (***************************************************************************) 11 12 (* possible values: 13 0 - no output at all (except for fatal errors) 14 1 - warnings only 15 2 - also diagnostic messages of constant length 16 3 - also diagnostic messages that are potentially lengthy (e.g., terms, 17 models, proofs) 18 4 - moreover, temporary files (for communication with the SMT solver) are 19 not removed after solver invocation *) 20 val trace = ref 2 21 22 val _ = Feedback.register_trace ("HolSmtLib", trace, 4) 23 24 (***************************************************************************) 25 (* I/O, parsing *) 26 (***************************************************************************) 27 28 (* opens 'path' as an output text file; writes all elements of 29 'strings' to this file (in the given order); closes the file *) 30 fun write_strings_to_file path strings = 31 let 32 val outstream = TextIO.openOut path 33 in 34 List.app (TextIO.output o Lib.pair outstream) strings; 35 TextIO.closeOut outstream 36 end 37 38 (* returns a function that returns the next character in 'instream' 39 and raises 'HOL_ERR' when at the end of 'instream' *) 40 fun get_buffered_char instream : unit -> char = 41 (* The fastest approach would be to slurp in the whole stream at 42 once. However, this is infeasible for long streams (especially 43 because 'String.explode' causes a significant memory 44 blowup). Reading chunks of 10000000 bytes (i.e., 10 MB) should be 45 a reasonable compromise between a small memory footprint (even 46 after 'String.explode') and a small number of reads. *) 47 let 48 val buffer = ref ([] : char list) 49 in 50 fn () => 51 (case !buffer of 52 [] => 53 (case String.explode (TextIO.inputN (instream, 10000000)) of 54 [] => 55 raise Feedback.mk_HOL_ERR "Library" "get_buffered_char" 56 "end of stream" 57 | c::cs => 58 (buffer := cs; c)) 59 | c::cs => 60 (buffer := cs; c)) 61 end 62 63 (* Takes a function that returns characters 64 (cf. 'get_buffered_char'), returns a function that returns 65 tokens. SMT-LIB 2 tokens are separated by whitespace (which is 66 dropped) or parentheses (which are tokens themselves). Tokens are 67 simply strings; we use no markup. *) 68 fun get_token (get_char : unit -> char) : unit -> string = 69 let 70 val buffer = ref (NONE : string option) 71 fun line_comment () = 72 if get_char () = #"\n" then 73 () 74 else line_comment () 75 fun aux_symbol cs c = 76 if c = #"|" then 77 (* we return |x| as x *) 78 String.implode (List.rev cs) 79 else 80 aux_symbol (c :: cs) (get_char ()) 81 fun aux_string cs c = 82 if c = #"\"" then 83 (* we return "x" as x *) 84 String.implode (List.rev cs) 85 else if c = #"\\" then 86 (* The only escape sequences in SMT-LIB are \" and \\. We simply drop 87 the backslash. *) 88 aux_string (get_char () :: cs) (get_char ()) 89 else 90 aux_string (c :: cs) (get_char ()) 91 fun (* whitespace *) 92 aux [] #" " = aux [] (get_char ()) 93 | aux [] #"\t" = aux [] (get_char ()) 94 | aux [] #"\n" = aux [] (get_char ()) 95 | aux [] #"\r" = aux [] (get_char ()) 96 | aux cs #" " = String.implode (List.rev cs) 97 | aux cs #"\t" = String.implode (List.rev cs) 98 | aux cs #"\n" = String.implode (List.rev cs) 99 | aux cs #"\r" = String.implode (List.rev cs) 100 (* parentheses *) 101 | aux [] #"(" = "(" 102 | aux [] #")" = ")" 103 | aux cs #"(" = (buffer := SOME "("; String.implode (List.rev cs)) 104 | aux cs #")" = (buffer := SOME ")"; String.implode (List.rev cs)) 105 (* | *) 106 | aux [] #"|" = aux_symbol [] (get_char ()) 107 | aux _ #"|" = 108 raise Feedback.mk_HOL_ERR "Library" "get_token" "invalid '|'" 109 (* " *) 110 | aux [] #"\"" = aux_string [] (get_char ()) 111 | aux _ #"\"" = 112 raise Feedback.mk_HOL_ERR "Library" "get_token" "invalid '\"'" 113 (* ; *) 114 | aux [] #";" = (line_comment (); aux [] (get_char ())) 115 | aux cs #";" = (line_comment (); String.implode (List.rev cs)) 116 (* everything else *) 117 | aux cs c = aux (c :: cs) (get_char ()) 118 handle Feedback.HOL_ERR _ => 119 (* end of stream *) 120 String.implode (List.rev (c :: cs)) 121 in 122 fn () => 123 let 124 val token = case !buffer of 125 SOME token => (buffer := NONE; token) 126 | NONE => aux [] (get_char ()) 127 in 128 if !trace > 2 then 129 Feedback.HOL_MESG ("HolSmtLib: next token is '" ^ token ^ "'") 130 else (); 131 token 132 end 133 end 134 135 fun parse_arbnum (s : string) = 136 Arbnum.fromString s 137 handle Option.Option => 138 raise Feedback.mk_HOL_ERR "Library" "parse_arbnum" 139 ("numeral expected, but '" ^ s ^ "' found") 140 141 fun expect_token (expected : string) (actual : string) : unit = 142 if expected = actual then 143 () 144 else 145 raise Feedback.mk_HOL_ERR "Library" "expect_token" 146 ("'" ^ expected ^ "' expected, but '" ^ actual ^ "' found") 147 148 (* extends a dictionary that maps keys to lists of values *) 149 fun extend_dict ((key, value), dict) = 150 let 151 val values = Redblackmap.find (dict, key) 152 handle Redblackmap.NotFound => [] 153 in 154 Redblackmap.insert (dict, key, value :: values) 155 end 156 157 (* entries in 'dict2' are prepended to entries in 'dict1' *) 158 fun union_dict dict1 dict2 = Redblackmap.foldl (fn (key, vals, dict) => 159 let 160 val values = Redblackmap.find (dict1, key) 161 handle Redblackmap.NotFound => [] 162 in 163 Redblackmap.insert (dict, key, vals @ values) 164 end) dict1 dict2 165 166 (* creates a dictionary that maps strings to lists of parsing functions *) 167 fun dict_from_list xs 168 : (string, (string -> Arbnum.num list -> 'a list -> 'a) list) 169 Redblackmap.dict = 170 List.foldl extend_dict (Redblackmap.mkDict String.compare) xs 171 172 (***************************************************************************) 173 (* Derived rules *) 174 (***************************************************************************) 175 176 (* A |- ... /\ t /\ ... 177 -------------------- 178 A |- t *) 179 fun conj_elim (thm, t) = 180 let 181 fun elim conj = 182 if Term.aconv t conj then 183 Lib.I 184 else 185 let 186 val (l, r) = boolSyntax.dest_conj conj 187 in 188 elim l o Thm.CONJUNCT1 189 handle Feedback.HOL_ERR _ => 190 elim r o Thm.CONJUNCT2 191 end 192 in 193 elim (Thm.concl thm) thm 194 end 195 196 (* A |- t 197 -------------------- 198 A |- ... \/ t \/ ... *) 199 fun disj_intro (thm, disj) = 200 if Term.aconv (Thm.concl thm) disj then 201 thm 202 else 203 let 204 val (l, r) = boolSyntax.dest_disj disj 205 in 206 Thm.DISJ1 (disj_intro (thm, l)) r 207 handle Feedback.HOL_ERR _ => 208 Thm.DISJ2 l (disj_intro (thm, r)) 209 end 210 211 (* auxiliary function: fails unless 's' is a subterm of 't' with 212 respect to 'destfn' *) 213 fun check_subterm destfn s t = 214 if Term.aconv s t then 215 () 216 else 217 let 218 val (l, r) = destfn t 219 in 220 check_subterm destfn s l 221 handle Feedback.HOL_ERR _ => 222 check_subterm destfn s r 223 end 224 225 (* |- ... \/ t \/ ... \/ ~t \/ ... *) 226 fun gen_excluded_middle disj = 227 let 228 val (pos, neg) = Lib.tryfind (fn neg => 229 let 230 val pos = boolSyntax.dest_neg neg 231 val _ = check_subterm boolSyntax.dest_disj pos disj 232 in 233 (pos, neg) 234 end) (boolSyntax.strip_disj disj) 235 val th1 = disj_intro (Thm.ASSUME pos, disj) 236 val th2 = disj_intro (Thm.ASSUME neg, disj) 237 in 238 Thm.DISJ_CASES (Thm.SPEC pos boolTheory.EXCLUDED_MIDDLE) th1 th2 239 end 240 241 (* A |- ... /\ t /\ ... /\ ~t /\ ... 242 --------------------------------- 243 A |- F *) 244 fun gen_contradiction thm = 245 let 246 val (pos, neg) = Lib.tryfind (fn neg => 247 let 248 val pos = boolSyntax.dest_neg neg 249 val _ = check_subterm boolSyntax.dest_conj pos (Thm.concl thm) 250 in 251 (pos, neg) 252 end) (boolSyntax.strip_conj (Thm.concl thm)) 253 val th1 = conj_elim (thm, pos) 254 val th2 = conj_elim (thm, neg) 255 in 256 Thm.MP (Thm.NOT_ELIM th2) th1 257 end 258 259 (***************************************************************************) 260 (* Tactics *) 261 (***************************************************************************) 262 263 (* A tactic that unfolds operations of set theory, replacing them by 264 propositional logic (representing sets as predicates). *) 265 val SET_SIMP_TAC = 266 let 267 val thms = [pred_setTheory.SPECIFICATION, pred_setTheory.GSPEC_ETA, 268 pred_setTheory.EMPTY_DEF, pred_setTheory.UNIV_DEF, 269 pred_setTheory.UNION_DEF, pred_setTheory.INTER_DEF] 270 in 271 simpLib.SIMP_TAC (simpLib.mk_simpset [pred_setTheory.SET_SPEC_ss]) thms 272 end 273 274 (* A tactic that unfolds LET. *) 275 val LET_SIMP_TAC = 276 simpLib.SIMP_TAC (simpLib.mk_simpset [boolSimps.LET_ss]) [] 277 278 (* A tactic that simplifies certain word expressions. *) 279 280 val TO_WORD_EXTRACT = Q.prove( 281 `(!w : 'a word. 282 dimindex(:'b) < dimindex(:'a) ==> 283 (w2w w : 'b word = (dimindex(:'b) - 1 >< 0) w)) /\ 284 (!w : 'a word. 285 dimindex(:'b) < dimindex(:'a) ==> 286 (sw2sw w : 'b word = (dimindex(:'b) - 1 >< 0) w))`, 287 BasicProvers.SRW_TAC [wordsLib.WORD_BIT_EQ_ss] []) 288 289 val WORD_BIT_EXTRACT = simpLib.SIMP_PROVE 290 (simpLib.++(bossLib.std_ss, wordsLib.WORD_BIT_EQ_ss)) 291 [wordsLib.WORD_DECIDE ``1w :word1 ' 0``] 292 ``!w:'a word i. i < dimindex (:'a) ==> (w ' i = ((i >< i) w = 1w:word1))`` 293 294 val WORD_SHIFT_BV = simpLib.SIMP_PROVE bossLib.bool_ss 295 [wordsTheory.word_shift_bv] 296 ``(!w:'a word n. n < dimword (:'a) ==> (w << n = w <<~ n2w n)) /\ 297 (!w:'a word n. n < dimword (:'a) ==> (w >> n = w >>~ n2w n)) /\ 298 (!w:'a word n. n < dimword (:'a) ==> (w >>> n = w >>>~ n2w n))`` 299 300 val bit_field_insert_rwt = simpLib.SIMP_RULE 301 (simpLib.++(bossLib.bool_ss, boolSimps.LET_ss)) [] wordsTheory.bit_field_insert; 302 303 val WORD_SIMP_TAC = let 304 open Tactical Conv Tactic wordsTheory simpLib 305 in 306 CONV_TAC (DEPTH_CONV wordsLib.EXPAND_REDUCE_CONV) THEN 307 SIMP_TAC (pureSimps.pure_ss ++ numSimps.REDUCE_ss ++ wordsLib.SIZES_ss) 308 [word_rol_bv_def, word_ror_bv_def, 309 w2n_n2w, word_bit_def, bit_field_insert_rwt, 310 word_lsb_def, word_msb_def, 311 WORD_SLICE_THM, WORD_BITS_EXTRACT, 312 WORD_BIT_EXTRACT, WORD_SHIFT_BV, TO_WORD_EXTRACT] THEN 313 CONV_TAC (DEPTH_CONV wordsLib.EXTEND_EXTRACT_CONV) 314 end 315 316(* 317 val WORD_SIMP_TAC = 318 simpLib.SIMP_TAC (simpLib.++ (bossLib.pure_ss, wordsLib.WORD_ss)) 319 [wordsTheory.EXTRACT_ALL_BITS, wordsTheory.WORD_EXTRACT_ZERO, 320 wordsTheory.LSL_LIMIT, wordsTheory.LSR_LIMIT] 321*) 322 323end 324