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