1 2(* user interface to HolCheck *) 3structure holCheck :> holCheck = 4struct 5 6local 7 8 open Globals HolKernel Parse 9 open bddTools ksTools ctlCheck cearTools modelTools internalCacheTools 10 11 val dpfx = "hc_" 12 13 fun init model = 14 let val _ = dbgTools.DEN dpfx "i"(*DBG*) 15 val _ = if bdd.isRunning() then () else bdd.init 1000000 10000 (* FIXME: allow user to supply the nums here *) 16 val (I1,T1,Ric,ksname,bvm,state,fl,_,ic) = dest_model model 17 val state = if isSome state then valOf state else mk_state I1 T1 18 val (apl,apsubs) = if get_flag_abs model then holCheckTools.mk_abs_APs fl state else (NONE,[]) 19 val vm = mk_varmap state bvm 20 val _ = dbgTools.DEX dpfx "i"(*DBG*) 21 in (I1,T1,Ric,ksname,bvm,state,fl,ic,vm,apl,apsubs) end 22 23in 24 25fun holCheck model = 26 let val _ = dbgTools.DEN dpfx "hc"(*DBG*) 27 val _ = profTools.bgt (dpfx^"hc")(*PRF*) 28 val (I1,T1,Ric,ksname,bvm,state,fl,ic,vm,apl,apsubs) = init model 29 val (results,ic) = 30 List.foldl (fn ((nf,f),(results,ic)) => 31 let 32 val _ = dbgTools.DST (dpfx^"hc_nf: "^nf) (*DBG*) 33 val is_mu = ((String.compare(fst(dest_type(type_of f)),"mu"))=EQUAL) 34 val (res,ic) = 35 if is_mu 36 then let val (r,(i,c)) = absCheck I1 T1 state Ric vm ksname (get_abs ic,get_common ic) 37 (nf,f) (apl,apsubs) 38 in (r,((set_common c) o (set_abs i)) ic) end 39 else let val (r,(i,c)) = ctlCheck I1 T1 state Ric vm ksname (get_ctl ic,get_common ic) 40 (nf,f) (apl,apsubs) 41 in (r,((set_common c) o (set_ctl i)) ic) end 42 in (results@[res],ic) end) 43 ([],if isSome ic then valOf ic else set_vm vm empty_ic) fl 44 val _ = profTools.ent (dpfx^"hc")(*PRF*) 45 val _ = dbgTools.DEX dpfx "hc"(*DBG*) 46 in (((set_ic ic) o (set_results results)) model) end 47 48end 49end 50