1
2(* miscellaneous useful stuff that doesn't fit in anywhere else *)
3structure satCommonTools =
4struct
5
6local
7
8open Globals HolKernel Parse boolSyntax Term Drule
9open satTheory
10
11in
12
13structure RBM = Redblackmap
14
15fun rbapply m k = RBM.find(m,k)
16
17fun tryrbapplyd m k d = rbapply m k handle NotFound => d
18
19
20fun pair_map f (x,y) = (f x,f y)
21
22(*********** terms **************)
23
24val mk_var = Term.mk_var;
25
26val land = rand o rator
27
28fun is_T tm = Term.compare(tm,T)=EQUAL
29
30fun is_F tm = Term.compare(tm,F)=EQUAL
31
32fun termFromFile fname =
33    let val ins        = TextIO.openIn (fname^".term")
34        val res        = TextIO.inputAll ins
35        val _          = TextIO.closeIn ins
36    in Term [QUOTE res] end
37
38fun termToFile fname t =
39let val fout = TextIO.openOut (fname^".term")
40    val _ = TextIO.output (fout,with_flag (show_types,true) term_to_string t)
41    val _ = TextIO.flushOut fout
42    val _ = TextIO.closeOut fout
43in () end
44
45(************ HOL **************)
46
47local
48    val t = mk_var("t",bool)
49    val NOT_NOT2 = SPEC_ALL NOT_NOT
50in
51fun NOT_NOT_CONV tm = INST [t|->rand(rand tm)] NOT_NOT2
52end
53
54(* Like CONJUNCTS but assumes the conjunct is bracketed right-assoc. *)
55(* Not tail recursive. Here only as a reference implementation *)
56fun NTL_CONJUNCTSR th =
57    if is_conj (concl th)
58    then
59        let val (th1,th2) = CONJ_PAIR th
60        in th1::(NTL_CONJUNCTSR th2) end
61    else [th]
62
63(* CPS version of NTL_CONJUNCTSR. Does not grow call stack. *)
64fun CONJUNCTSR th =
65    let fun CPS_CONJUNCTSR th k =
66            if is_conj (concl th)
67            then let val (th1,th2) = CONJ_PAIR th
68                 in CPS_CONJUNCTSR th2 (fn ret => k (th1::ret)) end
69            else k [th]
70    in CPS_CONJUNCTSR th I end
71
72end
73end
74