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