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