1 2structure cearTools = 3struct 4 5local 6 7open Globals HolKernel Parse 8 9open boolSyntax pairSyntax pairTools PairRules bossLib Tactical Tactic 10 Drule Rewrite pred_setTheory boolTheory Conv pairTheory 11 pred_setTheory pred_setLib stringLib listTheory rich_listTheory 12 simpLib pairLib PrimitiveBddRules DerivedBddRules Binarymap 13 HolSatLib sumSyntax numSyntax 14 15open cearTheory ksTheory setLemmasTheory muSyntaxTheory muSyntax 16 muTheory muTools ksTheory muCheck bddTools envTheory ksTools 17 commonTools lazyTools lzPairRules lzConv 18 19val _ = numLib.prefer_num(); 20 21val dpfx = "crt_" 22 23in 24 25val _ = set_trace "notify type variable guesses" 0; 26val abs_ks_tm = ``cear$ABS_KS`` 27val is_abs_fun_tm = ``cear$IS_ABS_FUN`` 28val _ = set_trace "notify type variable guesses" 1; 29 30fun get_astate_ty hname = (snd o pairSyntax.dest_prod o hd o snd o dest_type o type_of) hname 31 32(* prove that ABS_KS ks h = aks *) 33(* where hd is the definition h(s,sh) = ... (required only to get our hands on the constant h) *) 34fun mk_abs_eq_thm state state' astate astate' n hd_def ks_def aks_def goal = 35 prove(goal, 36 REWRITE_TAC [GSYM hd_def] 37 THEN REWRITE_TAC [ks_def,aks_def,ABS_KS_def,KS_component_equality,KS_accfupds,combinTheory.K_DEF] 38 THEN BETA_TAC 39 THEN REPEAT CONJ_TAC THENL 40 [ 41 REWRITE_TAC [EXTENSION] 42 THEN CONV_TAC (PairRules.GEN_PALPHA_CONV astate) 43 THEN PairRules.PGEN_TAC 44 THEN CONV_TAC (RHS_CONV pred_setLib.SET_SPEC_CONV) 45 THEN CONV_TAC (RHS_CONV (PairRules.GEN_PALPHA_CONV state)) 46 THEN CONV_TAC (RHS_CONV commonTools.ELIM_TUPLED_QUANT_CONV) 47 THEN SIMP_TAC std_ss [IN_DEF,CONJ_COMM] THEN PairRules.PBETA_TAC, (* S0 *) 48 CONV_TAC (RHS_CONV (ABS_CONV (GEN_PALPHA_CONV (mk_pair(astate,astate'))))) 49 THEN CONV_TAC (RHS_CONV (PABS_CONV (PABS_CONV(QUANT_CONV(GEN_PALPHA_CONV state'))))) 50 THEN CONV_TAC (RHS_CONV (ABS_CONV (PABS_CONV(GEN_PALPHA_CONV state)))) 51 THEN PBETA_TAC 52 THEN REFL_TAC, (* T *) 53 REWRITE_TAC [SET_SPEC,BIGUNION] 54 THEN ONCE_REWRITE_TAC [FUN_EQ_THM] 55 THEN CONV_TAC (GEN_PALPHA_CONV astate) 56 THEN PairRules.PGEN_TAC 57 THEN CONV_TAC (FORK_CONV(PBETA_CONV,PBETA_CONV)) 58 THEN ONCE_REWRITE_TAC [FUN_EQ_THM] 59 THEN GEN_TAC 60 THEN CONV_TAC (FORK_CONV(PBETA_CONV,ONCE_REWRITE_CONV [GSYM SPECIFICATION])) 61 THEN CONV_TAC (RHS_CONV (SIMP_CONV std_ss [SET_SPEC])) 62 THEN CONV_TAC (RHS_CONV (QUANT_CONV (LAND_CONV(GEN_PALPHA_CONV state)))) 63 THEN PBETA_TAC 64 THEN CONV_TAC (RHS_CONV (QUANT_CONV (LAND_CONV commonTools.ELIM_TUPLED_QUANT_CONV))) 65 THEN NTAC n (CONV_TAC (RHS_CONV (STRIP_QUANT_CONV LEFT_AND_EXISTS_CONV))) 66 THEN RW_TAC std_ss [IN_DEF] 67 THEN REFL_TAC 68 ]) 69 70(* abs_fun is (ap_0 = av_0) /\ (ap_1 = av_1) /\ ... where the ap_i are atomic propositions extracted (currently) from the properties to 71 be checked. Thus the size of the abstract state is the same as the total number of atomic props over all the properties. 72 In case this is >= the number of concrete state vars (possible in very small models), hct.maA ensures we do not bother abstracting *) 73fun mk_abs_fun aapl vm state hname = 74 let val _ = dbgTools.DEN dpfx "maf" (*DBG*) 75 val state' = mk_primed_state state 76 val nabsv = List.length aapl (* # of abs state vars needed *) 77 (*FIXME: what happens if there is a concrete state var called av_i? bad things *) 78 val astate = pairSyntax.list_mk_pair(List.tabulate(nabsv,fn i => mk_bool_var("av"^(int_to_string i)))) 79 val vm = List.foldl (* add any newly created abstract vars to the varmap *) 80 (fn (v,bm) => 81 if isSome(Binarymap.peek(bm,v)) then bm 82 else let val n = Binarymap.numItems bm 83 in Binarymap.insert(Binarymap.insert(bm,v,n+1),v^"'",n) end) 84 vm (List.map term_to_string (strip_pair astate)) 85 val _ = if (bdd.getVarnum()<(Binarymap.numItems vm)) 86 then bdd.setVarnum (Binarymap.numItems vm) else () 87 (*FIXME: it would be nice to use Lexis.nameStrm here, but then need to restructure init_abs to return stuff other than 88 what comes from the cache, since I want to be able to eventually persist the cache, and nameStrm is a closure *) 89 val hn = if (isSome hname) then valOf hname else "af" 90 val _ = new_constant(hn,(mk_prod(type_of state,type_of astate)) --> bool) 91 val hnc = mk_const(hn,(mk_prod(type_of state,type_of astate)) --> bool) 92 val apl = List.map pbody aapl 93 val apll = listSyntax.mk_list (apl,bool) 94 val ast = strip_pair astate 95 val shl = listSyntax.mk_list (ast,bool) 96 val hd_def = hd(Defn.eqns_of(Hol_defn hn 97 `(^hnc) (^state,^(astate)) = AND_EL (MAP (UNCURRY $=) (ZIP(^apll,^shl)))`)) 98 val utjf = (fn _ => CONV_RULE (STRIP_QUANT_CONV (RHS_CONV ((funpow (nabsv-1) RAND_CONV) (* get rid of trailing ``/\ T`` *) 99 (PURE_ONCE_REWRITE_CONV [AND_CLAUSES])))) 100 (PURE_REWRITE_RULE 101 [MAP,ZIP,UNCURRY_DEF,AND_EL_DEF,combinTheory.I_THM,combinTheory.C_THM,ALL_EL] hd_def)) 102 val utgl = list_mk_forall(((strip_pair state)@ast), 103 mk_eq(lhs(snd(strip_forall(concl hd_def))), 104 list_mk_conj(List.map mk_eq (ListPair.zip(apl,ast))))) 105 val unwind_thm = mk_lthm (fn _ => (utgl,utjf)) utjf 106 val _ = dbgTools.CBTH (dpfx^"maf_unwind_thm") unwind_thm 107 val _ = lazyTools.testlz (dpfx^"maf_unwind_thm") utjf unwind_thm 108 val abs_fun = BddEqMp (SYM (SPEC_ALL unwind_thm)) (t2tb vm (rhs(snd(strip_forall(concl unwind_thm))))) 109 val _ = dbgTools.DTH (dpfx^"maf_ hd_def") hd_def (*DBG*) 110 val _ = dbgTools.DEX dpfx "maf" (*DBG*) 111 in (astate,unwind_thm,Binarymap.mkDict Int.compare,hd_def,abs_fun) end 112 113 114(* prove that the concrete abs_funs is total, by building the bdd *) 115(* FIXME: can we prove this offline by completely formalizing the construction of the abs fun? *) 116fun mk_abs_fun_total_thm abs_fun = 117 let val _ = dbgTools.DEN dpfx "maftt" (*DBG*) 118 val (st,ast) = (strip_pair ## strip_pair) (dest_pair(snd(dest_comb(getTerm abs_fun)))) 119 val gl = mk_pforall(list_mk_pair st, mk_pexists(list_mk_pair ast,getTerm abs_fun)) 120 val jf = (fn _ => (REWRITE_RULE [SYM (CONV_RULE (RHS_CONV (STRIP_QUANT_CONV ELIM_TUPLED_QUANT_CONV)) 121 (ELIM_TUPLED_QUANT_CONV gl))] 122 (BddThmOracle(BddForall st (BddExists ast abs_fun))))) 123 val res = mk_lthm (fn _ => (gl,jf)) jf 124 val _ = lazyTools.testlz (dpfx^"maftt_res") jf res 125 val _ = dbgTools.DTH (dpfx^"maftt_res") res (*DBG*) 126 val _ = dbgTools.DEX dpfx "maftt" (*DBG*) 127 in res end 128 129(* function that alpha-convs IS_ABS_FUN_def to use concrete state, astate and h *) 130(* FIXME: clean this up*) 131fun mk_conc_is_abs_fun_def st1 st2 state astate abs_fun ks_def = 132 let val _ = dbgTools.DEN dpfx "mciafd" (*DBG*) 133 val hit_tot = STRIP_QUANT_CONV o RHS_CONV o LAND_CONV 134 val th = INST_TYPE [``:'state`` |-> type_of st1, ``:'astate`` |-> type_of astate] IS_ABS_FUN_def 135 val th1 = CONV_RULE (hit_tot (QUANT_CONV (GEN_PALPHA_CONV astate))) th 136 val th2 = CONV_RULE (hit_tot (GEN_PALPHA_CONV state)) th1 137 val hit_ap = STRIP_QUANT_CONV o RHS_CONV o RAND_CONV 138 val th3 = CONV_RULE (hit_ap (QUANT_CONV (QUANT_CONV (GEN_PALPHA_CONV astate)))) th2 139 val th4 = CONV_RULE (hit_ap (QUANT_CONV (GEN_PALPHA_CONV st2))) th3 140 val th5 = CONV_RULE (hit_ap (GEN_PALPHA_CONV st1)) th4 141 val aht = mk_pabs(mk_pair(state,astate),getTerm abs_fun) 142 val ksname = lhs(concl ks_def) 143 val res = PBETA_RULE (GEN_ALL (ISPECL [ksname,mk_var("e",stringLib.string_ty-->(type_of st1)-->bool),aht] th5)) 144 val _ = dbgTools.DTH (dpfx^"mciafd_ cons is abs fun") res (*DBG*) 145 val _ = dbgTools.DEX dpfx "mciafd" (*DBG*) 146 in res end 147 148(* mk refined abstraction function and the is_abs_fun thm for it as well (to be used by mk_abs_cons_thm) *) 149(* as1 is the abs state that got split into dead and bad (which are conrete state sets) *) 150fun mk_ref_abs_fun af state astate ks_def ath_lem1 ath_lem2 hd_def idx as1 dead bad k = 151 let val _ = dbgTools.DEN dpfx "mraf" (*DBG*) 152 (*val nabsv = Real.ceil(log2(Real.fromInt(k+1))) (* to check if new abstract state requires another abs var to be added *)*) 153 val ast = strip_pair astate 154 val nabsv = (List.length ast)+1 (* FIXME: we add one abs var per refinement. could do better (see Mar 20, 2005, notes) *) 155 val vm = getVarmap af 156 val navn = "av"^(int_to_string(nabsv-1)) 157 val nav = mk_var(navn,bool) 158 val vmn = listmax(List.map snd (Binarymap.listItems vm))+1 (* can't use bddVarnum because the cnf stuff in ca' adds to it *) 159 val vm' = Binarymap.insert(Binarymap.insert(vm,navn,vmn+1),navn^"'",vmn) 160 val astate2 = list_mk_pair (nav::(strip_pair(astate))) 161 val _ = if (bdd.getVarnum()<((Binarymap.numItems vm'))) 162 then bdd.setVarnum ((Binarymap.numItems vm')) else () 163 val (navtb,nnavtb) = (BddVar true vm' nav,BddVar false vm' nav) 164 (* refined abs fun af' is (bad /\ nav /\ af) \/ (dead /\ ~nav /\ af) \/ (~bad /\ ~dead /\ af) *) 165 val (bad2,dead2,af2) = (BddExtendVarmap vm' bad,BddExtendVarmap vm' dead,BddExtendVarmap vm' af) 166 val _ = dbgTools.DBD (dpfx^"mraf_bad2_bdd") (getBdd bad2)(*DBG*) 167 val _ = dbgTools.DBD (dpfx^"mraf_dead2_bdd") (getBdd dead2)(*DBG*) 168 val _ = dbgTools.DBD (dpfx^"mraf_af2_bdd") (getBdd af2)(*DBG*) 169 val af' = BddListDisj vm' [BddListConj vm' [bad2,navtb,af2],BddListConj vm' [dead2,nnavtb,af2], 170 BddListConj vm' [BddNot bad2,BddNot dead2,af2]] 171 val _ = dbgTools.DBD (dpfx^"mraf_af'_bdd") (getBdd af')(*DBG*) 172 val hn = term_to_string2(rator(lhs(snd(strip_forall(concl hd_def)))))^"'" 173 val harg_ty = mk_prod(type_of state,type_of astate2) 174 val _ = new_constant(hn,harg_ty --> bool) 175 val hnc = mk_const(hn,harg_ty --> bool) 176 val hd_def2 = hd(Defn.eqns_of(Hol_defn hn `(^hnc)(^state,^(astate2)) = ^(getTerm af')`)) 177 val _ = dbgTools.DTH (dpfx^"mraf_hd_def2") hd_def2 (*DBG*) 178 val _ = dbgTools.CBTH (dpfx^"mraf_hd_def2") hd_def2 (*DBG*) 179 (* FIXME: the variant here does not really help avoid a name clash with vars already in state, because I add _1 etc*) 180 val vn = fst(dest_var(variant ((strip_pair state)@(strip_pair (mk_primed_state state))) ``v:bool``)) 181 val lst1 = List.tabulate(List.length (strip_pair state),fn n => mk_bool_var(vn^(int_to_string n)^"_1")) 182 val lst2 = List.tabulate(List.length (strip_pair state),fn n => mk_bool_var(vn^(int_to_string n)^"_2")) 183 val subst1 = ListPair.map (fn (v,v') => v |-> v') (strip_pair state,lst1) 184 val subst2 = ListPair.map (fn (v,v') => v |-> v') (strip_pair state,lst2) 185 val hd_lhs = lhs(snd(strip_forall(concl hd_def2))) 186 val goal = mk_imp(mk_conj(subst subst1 hd_lhs,subst subst2 hd_lhs),rand(concl ath_lem1)) 187 val _ = dbgTools.CBTM (dpfx^"mraf_goal") goal (*DBG*) 188 val _ = dbgTools.CBTH (dpfx^"mraf_ath_lem1") ath_lem1 (*DBG*) 189 val (al1ante1,al1ante2) = dest_conj(land(concl ath_lem1)) 190 val jfal1' = (fn _ => (*PURE_ONCE_REWRITE_RULE [GSYM hd_def2]*) (* prove new ath_lem1 using the old one *) 191 (prove(goal, 192 PURE_ONCE_REWRITE_TAC [hd_def2] 193 THEN RW_TAC pure_ss [] 194 THEN PAT_ASSUM al1ante1 (fn t1 => PAT_ASSUM al1ante2 (fn t2 => 195 LIST_ACCEPT_TAC (CONJUNCTS (MP (lazyTools.prove_lthm ath_lem1) (CONJ t1 t2)))) 196 )))) 197 val ath_lem1' = (*PURE_ONCE_REWRITE_RULE [GSYM hd_def2]*) (mk_lthm (fn _ => (goal,jfal1')) jfal1') 198 val _ = dbgTools.DTH (dpfx^"mraf_ath_lem1'") ath_lem1' (*DBG*) 199 val _ = dbgTools.CBTH (dpfx^"mraf_ath_lem1'") ath_lem1' (*DBG*) 200 val _ = lazyTools.testlz (dpfx^"mraf_ath_lem1'") jfal1' ath_lem1' 201 val _ = dbgTools.DTH (dpfx^"mraf_ath_lem2") ath_lem2 (*DBG*) 202 val _ = dbgTools.CBTH (dpfx^"mraf_ath_lem2") ath_lem2 (*DBG*) 203 val st1 = list_mk_pair lst1 204 val st2 = list_mk_pair lst2 205 val jfafap = (fn _ => (PGENL [st1,st2,astate2] (IMP_TRANS ath_lem1' (SPEC_ALL ath_lem2)))) 206 val afapgl = list_mk_pforall ([st1,st2,astate2],mk_imp((fst o dest_imp) (concl ath_lem1'), 207 (snd o dest_imp o snd o strip_forall) (concl ath_lem2))) 208 val afap = mk_lthm (fn _ => (afapgl,jfafap)) jfafap 209 val _ = dbgTools.DTH (dpfx^"mraf_afap") afap (*DBG*) 210 val _ = lazyTools.testlz (dpfx^"mraf_afap") jfafap afap 211 val af' = BddEqMp (SYM (SPEC_ALL hd_def2)) af' 212 val aftot = mk_abs_fun_total_thm af' 213 val jfiaf = (fn _ => (CONV_RULE (DEPTH_CONV PETA_CONV) 214 (REWRITE_RULE [GSYM hd_def2] (REWRITE_RULE [CONJ aftot afap] (mk_conc_is_abs_fun_def st1 st2 state astate2 af' ks_def))))) 215 val ksname = lhs(concl ks_def) 216 val ((p_ty,st_ty),ast_ty) = (get_types ksname,type_of astate2) 217 val e_var = inst [alpha |-> st_ty] envTools.env_tm 218 val iaf = mk_lthm (fn _ => (mk_forall(e_var,list_mk_comb(inst [alpha|->p_ty,beta|->st_ty,gamma|->ast_ty] is_abs_fun_tm, 219 [ksname,e_var,mk_const(hn,harg_ty --> bool)])), 220 jfiaf)) jfiaf 221 val _ = dbgTools.DTH (dpfx^"mraf_iaf") iaf (*DBG*) 222 val _ = lazyTools.testlz (dpfx^"mraf_iaf") jfiaf iaf 223 val _ = dbgTools.DEX dpfx "mraf" (*DBG*) 224 in (af',ath_lem1',astate2,hd_def2,iaf) end 225 226fun is_pabs_cond tm = 227 (can (match_term ``COND x y z``) tm) 228 andalso pairSyntax.is_pabs (#2(dest_cond tm)) andalso pairSyntax.is_pabs(#3(dest_cond tm)) 229 andalso Term.compare(fst (pairSyntax.dest_pabs (#2(dest_cond tm))),fst (pairSyntax.dest_pabs (#3(dest_cond tm))))=EQUAL 230 231(* any subterm of tm matching the pattern ``if b then \x. P else \x. Q`` is converted to ``\x. if b then P else Q`` *) 232fun ABS_COND_CONV tm = 233 if is_pabs_cond tm 234 then let val ab = fst (pairSyntax.dest_pabs (#2(dest_cond tm))) 235 in (REWRITE_CONV [GSYM COND_ABS] THENC PairRules.GEN_PALPHA_CONV ab THENC (DEPTH_CONV PairRules.PBETA_CONV)) tm end 236 else NO_CONV tm 237 238(* creates abstracted Tm and I and passes them to mk_wfKS and returns the results *) 239(* h is the abs_fun as returned by mk_abs_fun *) 240fun mk_abs_ks I1 ITdf RTm state astate Ric af aksname (apl,ks_def,wfKS_ks) hd_def = 241 let val _ = dbgTools.DEN dpfx "mak"(*DBG*) 242 val _ = profTools.bgt (dpfx^"mak") (*PRF*) 243 val _ = profTools.bgt (dpfx^"mak_init") (*PRF*) 244 val T1 = Binarymap.listItems RTm 245 val st = strip_pair state 246 val st_ty = type_of state 247 val state' = mk_primed_state state 248 val st' = strip_pair state' 249 val vm = getVarmap af 250 val s2s' = List.map (fn(v,v') => (BddVar true vm v,BddVar true vm v')) (ListPair.zip(st,st')) 251 val _ = List.app (fn (s,_) => dbgTools.DST (dpfx^ s) ) (Binarymap.listItems vm) val _ = dbgTools.DST (dpfx^ "vm\n") 252 val vmabs = List.filter (fn (t,_) => (String.size t) >= 3 andalso String.compare("av",String.substring(t,0,2))=EQUAL ) 253 (Binarymap.listItems vm) 254 val abst = strip_pair astate 255 val astate' = mk_primed_state astate 256 val abst' = strip_pair astate' 257 val abstcnj = t2tb vm (list_mk_conj abst) 258 val abstcnj' = t2tb vm (list_mk_conj abst') 259 val as2as' = List.map (fn(v,v') => (BddVar true vm v,BddVar true vm v')) (ListPair.zip(abst,abst')) 260 val _ = profTools.ent (dpfx^"mak_init") (*PRF*) 261 val _ = profTools.bgt (dpfx^"mak_Ih") (*PRF*) 262 val Itb = BddEqMp (SYM (fst (valOf ITdf))) (t2tb vm I1) (* abbrev Itb to use either ctlks.S0 or muks.S0 *) 263 val Ih = BddExists st (BddOp(bdd.And,af,Itb)) 264 val Iht = getTerm Ih 265 val _ = profTools.ent (dpfx^"mak_Ih") (*PRF*) 266 val _ = profTools.bgt (dpfx^"mak_Th") (*PRF*) 267 val Th = List.map (fn (actnm,act) => (actnm,BddExists st (BddExists st' 268 (BddOp(bdd.And,BddExtendVarmap vm act,BddOp(bdd.And,af,BddReplace as2as' (BddReplace s2s' af))))))) T1 269 val Th' = List.map (fn (nm,tb) => (nm, 270 BddEqMp (SYM ((lzELIM_TUPLED_QUANT_CONV THENC STRIP_QUANT_CONV lzELIM_TUPLED_QUANT_CONV) 271 (list_mk_pexists([state,state'],snd(strip_pexists(getTerm tb)))))) tb)) Th 272 val T1h = List.map (fn (nm,tb) => (nm,getTerm tb)) Th' 273 val _ = profTools.ent (dpfx^"mak_Th") (*PRF*) 274 val _ = profTools.bgt (dpfx^"mak_ks") (*PRF*) 275 val (aapl,aks_def,wfKS_aks,aRTm,_) = mk_wfKS Iht T1h (SOME (list2map Th')) astate vm Ric NONE 276 (SOME (af,getT (rhs(concl ks_def)),state,state')) (SOME aksname) 277 val _ = profTools.ent (dpfx^"mak_ks") (*PRF*) 278 val _ = profTools.ent (dpfx^"mak") (*PRF*) 279 val _ = dbgTools.DTH (dpfx^"mak_ aks_def") aks_def (*DBG*) 280 val _ = dbgTools.DTM (dpfx^"mak_ aks_def.T") (getT (rhs(concl aks_def))) (*DBG*) 281 val _ = dbgTools.DEX dpfx "mak"(*DBG*) 282 in (Iht,T1h,Ih,(aapl,aks_def,wfKS_aks,aRTm)) end 283 284(* |- aks = ABS_KS ks h *) 285fun mk_abs_aks_thm state astate af state' astate' st hd_def ks_def aks_def = 286 let val _ = dbgTools.DEN dpfx "makt"(*DBG*) 287 val jf = (fn _ => 288 let val aht = mk_pabs(mk_pair(state,astate),getTerm af) 289 val _ = dbgTools.DTM (dpfx^"makt_ goal") ``^(lhs (concl aks_def)) = ABS_KS ^(lhs (concl ks_def)) ^aht`` (*DBG*) 290 val _ = dbgTools.DTH (dpfx^"makt_ hd_def") hd_def (*DBG*) 291 val _ = dbgTools.DTH (dpfx^"makt_ ks_def") ks_def (*DBG*) 292 val _ = dbgTools.DTH (dpfx^"makt_ aks_def") aks_def (*DBG*) 293 val _ = dbgTools.DTM (dpfx^"makt_ aht") aht (*DBG*) 294 val aksth = mk_abs_eq_thm state state' astate astate' (List.length st) hd_def ks_def aks_def 295 ``^(lhs (concl aks_def)) = ABS_KS ^(lhs (concl ks_def)) ^aht`` 296 val abs_aks = CONV_RULE (RHS_CONV (RAND_CONV PETA_CONV)) aksth 297 in abs_aks end) 298 val (p_ty,st_ty,ast_ty) = (mk_type("fun",[type_of state,bool]),type_of state,type_of astate) 299 val ksname = lhs(concl ks_def) 300 val aksname = lhs(concl aks_def) 301 val hname = rator(lhs(concl(SPEC_ALL hd_def))) 302 val abs_aks = mk_lthm (fn _ => (mk_eq(aksname, 303 list_mk_comb(inst [alpha|->p_ty,beta|->st_ty,gamma|->ast_ty] abs_ks_tm,[ksname,hname])), 304 jf)) jf 305 val _ = dbgTools.DTH (dpfx^"makt_abs_aks") abs_aks (*DBG*) 306 val _ = dbgTools.CBTH (dpfx^"makt_abs_aks") abs_aks (*DBG*) 307 val _ = dbgTools.DEX dpfx "makt"(*DBG*) 308 in abs_aks end 309 310(* prove the second part of the IS_ABS_FUN assum (the first part is totality) *) 311fun mk_abs_fun_ap_thm state astate hR_defs_ unwind_thm (apl,ks_def,wfKS_ks) hd_def = 312 let val _ = dbgTools.DEN dpfx "mafat"(*DBG*) 313 val state' = mk_primed_state state 314 (*FIXME: will need to fix this once state vars can be other than bools *) 315 (* FIXME: the variant here does not really help avoid a name clash with vars already in state, because I add _1 etc*) 316 val vn = fst(dest_var(variant ((strip_pair state)@(strip_pair state')) ``v:bool``)) 317 val lst1 = List.tabulate(List.length (strip_pair state),fn n => mk_bool_var(vn^(int_to_string n)^"_1")) 318 val lst2 = List.tabulate(List.length (strip_pair state),fn n => mk_bool_var(vn^(int_to_string n)^"_2")) 319 val st1 = list_mk_pair lst1 (*the s1 in IS_ABS_FUN_ap*) 320 val st2 = list_mk_pair lst2 (*the s2 in IS_ABS_FUN_ap*) 321 val st2vw = List.map (op |->) (ListPair.zip((strip_pair state)@(strip_pair state'),lst1@lst2)) 322 val (lht,rht) = dest_eq(snd(strip_forall(concl hd_def))) 323 val _ = dbgTools.DTH (dpfx^"mafat_ hd_def") hd_def (*DBG*) 324 val ath_lem1 = hd (CONJUNCTS (PURE_ONCE_REWRITE_RULE [EQ_IMP_THM] 325 (ONCE_REWRITE_CONV [unwind_thm] (mk_conj (subst [state|->st1] lht,subst [state|->st2] lht))))) 326 val _ = dbgTools.DTH (dpfx^"mafat_ath_lem1") ath_lem1 (*DBG*) 327 val _ = dbgTools.CBTH (dpfx^"mafat_ath_lem1") ath_lem1 (*DBG*) 328 val ksname = lhs(concl ks_def) 329 val ap_eqs = rand(concl ath_lem1) (*(ap0 = av0) /\ (ap1 = av1) /\ ... *) 330 val _ = dbgTools.DTM (dpfx^"mafat_ap_eqs") ap_eqs (*DBG*) 331 val gl2 = mk_forall(mk_var("e",stringLib.string_ty --> (type_of state) --> bool), 332 mk_imp(ap_eqs,``!p. p IN (^ksname).ap ==> 333 ((^st1) IN STATES (AP p) (^ksname) e = (^st2) IN STATES (AP p) (^ksname) e)``)) 334 val jf2 = (fn _ => 335 let val apl' = List.map (fn ap => mk_pabs(st2,subst (List.map (fn (v,w) => v |-> w) 336 (ListPair.zip(lst1,lst2))) (pbody ap))) apl 337 val ap_thms = List.map (*FIXME:clean this up, too much duplication in creation of the msa's, Lth and gen_ap_thms*) 338 (fn th => PURE_ONCE_REWRITE_RULE [MU_SAT_def] (GSYM th)) 339 (let val (prop_type,state_type) = get_types ksname 340 val Lth = ksTools.mk_Lth ks_def 341 val (msa1,msa2) = pair_map (fn t => PBETA_RULE (PURE_REWRITE_RULE [Lth] (MATCH_MP 342 (CONV_RULE FORALL_IMP_CONV (ISPECL [t,ksname] MU_SAT_AP)) wfKS_ks))) (st1,st2) 343 in (List.map (fn mf =>muCheck.mk_gen_ap_thm ksname st1 msa1 mf)(List.map (fn ap => ``AP ^ap``) apl)) 344 @ (List.map (fn mf =>muCheck.mk_gen_ap_thm ksname st2 msa2 mf)(List.map (fn ap =>``AP ^ap``) apl')) 345 end) 346 val _ = dbgTools.DST (dpfx^"mafat_ before ath_lem2") (*DBG*) 347 val _ = dbgTools.CBTM (dpfx^"mafat_gl2") gl2(*DBG*) 348 val _ = dbgTools.CBTHL (dpfx^"mafat_ksthl") [lazyTools.prove_lthm ks_def,KS_accfupds,combinTheory.K_DEF] (*DBG*) 349 val _ = dbgTools.CBTHL (dpfx^"mafat_fstthl") (List.map lazyTools.prove_lthm (ap_thms)) (*DBG*) 350 val ath_lem2 = prove(gl2, (* note we unlazify any thms used in any proof that uses tactics (VALID fails otherwise)*) 351 NTAC 3 STRIP_TAC 352 THEN CONV_TAC (LAND_CONV (PURE_REWRITE_CONV [lazyTools.prove_lthm ks_def, 353 KS_accfupds,combinTheory.K_DEF])) 354 THEN BETA_TAC 355 THEN RW_TAC pure_ss [IN_INSERT,NOT_IN_EMPTY] 356 THEN ASM_REWRITE_TAC (List.map lazyTools.prove_lthm (ap_thms))) 357 val _ = dbgTools.CBTH (dpfx^"mafat_ath_lem2") ath_lem2(*DBG*) 358 val _ = dbgTools.DTH (dpfx^"mafat_ath_lem2") ath_lem2 (*DBG*) 359 in ath_lem2 end) 360 val ath_lem2 = mk_lthm (fn _ => (gl2,jf2)) jf2 361 val _ = lazyTools.testlz (dpfx^"mafat_ath_lem2") jf2 ath_lem2 362 val jfap = (fn _ => PGENL [st1,st2,astate] (IMP_TRANS ath_lem1 (SPEC_ALL ath_lem2))) 363 val afap = mk_lthm (fn _ => (list_mk_pforall([st1,st2,astate],mk_imp(land(concl ath_lem1), 364 rand(snd(strip_forall(concl ath_lem2))))), jfap)) jfap 365 val _ = lazyTools.testlz (dpfx^"mafat_afap") jfap afap 366 val _ = dbgTools.DEX dpfx "mafat"(*DBG*) 367 in (st1,st2,ath_lem1,ath_lem2,afap) end 368 369local 370 371val Qvar = mk_var("Q",stringLib.string_ty) 372val gvar = mk_var("g",mu_ty) 373val avar = mk_var("a",stringLib.string_ty) 374fun pvar p_ty = mk_var("p",p_ty) 375fun mk_glno_rv p_ty f = 376 mk_forall(Qvar,mk_neg(list_mk_comb(get_mu_ty_sub_tm p_ty, 377 [mu_neg(mu_RV p_ty Qvar), 378 mk_comb(get_mu_ty_nnf_tm p_ty,f)]))) 379fun mk_glno_dmd p_ty f = 380 let val g = inst [alpha|->p_ty] gvar 381 in list_mk_forall([avar,g],mk_neg(list_mk_comb(get_mu_ty_sub_tm p_ty, 382 [mu_dmd avar g,mk_comb(get_mu_ty_nnf_tm p_ty,f)]))) end 383fun mk_glp_in_ap p_ty f ksname = 384 let val p = pvar p_ty 385 in mk_forall(p,mk_imp(list_mk_comb(get_mu_ty_sub_tm p_ty,[mu_AP p,f]), 386 list_mk_comb(inst [alpha|->p_ty] pred_setSyntax.in_tm,[p,mk_ks_dot_ap ksname]))) end 387 388in 389(* prove the three formula related assumptions to ABS_CONS_MODEL *) 390fun mk_abs_cons_mf_thms mf (apl,ks_def,wfKS_ks) vm = 391let val _ = dbgTools.DEN dpfx "macmt"(*DBG*) 392 val _ = profTools.bgt (dpfx^"macmt")(*PRF*) 393 val ksname = lhs(concl ks_def) 394 val (p_ty,s_ty) = get_types ksname 395 val _ = profTools.bgt (dpfx^"macmt_no_rv")(*PRF*) 396 val _ = profTools.bgt (dpfx^"macmt_no_rv_gl")(*PRF*) 397 val glno_rv = mk_glno_rv p_ty mf (*``!Q. ~SUBFORMULA (~RV Q) (NNF (^mf))``*) 398 val _ = profTools.ent (dpfx^"macmt_no_rv_gl")(*PRF*) 399 val jfno_rv = (fn _ => (prove (glno_rv,SIMP_TAC std_ss (MU_SUB_def::NNF_def::RVNEG_def::(tsimps ``:'a mu``))))) 400 val no_rv = mk_lthm (fn _ => (glno_rv,jfno_rv)) jfno_rv 401 val _ = lazyTools.testlz (dpfx^"macmt_no_rv") jfno_rv no_rv(*DBG*) 402 val _ = profTools.ent (dpfx^"macmt_no_rv")(*PRF*) 403 val _ = profTools.bgt (dpfx^"macmt_no_dmd")(*PRF*) 404 val _ = profTools.bgt (dpfx^"macmt_no_dmd_gl")(*PRF*) 405 val glno_dmd = mk_glno_dmd p_ty mf (*``(!a g. ~SUBFORMULA <<a>> g (NNF (^mf)))``*) 406 val _ = profTools.ent (dpfx^"macmt_no_dmd_gl")(*PRF*) 407 val jfno_dmd = (fn _ => (prove (glno_dmd,Induct_on `g` THEN SIMP_TAC std_ss (MU_SUB_def::NNF_def::RVNEG_def::(tsimps ``:'a mu``))))) 408 val no_dmd = mk_lthm (fn _ => (glno_dmd,jfno_dmd)) jfno_dmd 409 val _ = lazyTools.testlz (dpfx^"macmt_no_dmd") jfno_dmd no_dmd(*DBG*) 410 val _ = profTools.ent (dpfx^"macmt_no_dmd")(*PRF*) 411 val _ = profTools.bgt (dpfx^"macmt_p_in_ap")(*PRF*) 412 val _ = profTools.bgt (dpfx^"macmt_p_in_ap_gl")(*PRF*) 413 val glp_in_ap = mk_glp_in_ap p_ty mf ksname (*``!p. SUBFORMULA (AP p) (^mf) ==> p IN (^(lhs(concl ks_def))).ap``*) 414 val _ = dbgTools.CBTM (dpfx^"macmt_glp") glp_in_ap (*DBG*) 415 val _ = dbgTools.CBTHL (dpfx^"macmt_glpl1") (ks_def::KS_accfupds::combinTheory.K_DEF::MU_SUB_def::NNF_def::RVNEG_def::(tsimps ``:'a mu``)) 416 val _ = profTools.ent (dpfx^"macmt_p_in_ap_gl")(*PRF*) 417 val jfp_in_ap = (fn _ => (prove (glp_in_ap, 418 PURE_REWRITE_TAC (*SIMP_TAC std_ss *) 419 (List.map lazyTools.prove_lthm 420 (ks_def::KS_accfupds::combinTheory.K_DEF::MU_SUB_def::NNF_def::RVNEG_def::(tsimps ``:'a mu``))) 421 THEN BETA_TAC 422 THEN RW_TAC pure_ss [] 423 THEN CONV_TAC (pred_setLib.IN_CONV (AP_EQ vm))))) 424 val p_in_ap = mk_lthm (fn _ => (glp_in_ap,jfp_in_ap)) jfp_in_ap 425 val _ = lazyTools.testlz (dpfx^"macmt_p_in_ap") jfp_in_ap p_in_ap(*DBG*) 426 val _ = profTools.ent (dpfx^"macmt_p_in_ap")(*PRF*) 427 val _ = profTools.ent (dpfx^"macmt")(*PRF*) 428 val _ = dbgTools.DEX dpfx "macmt"(*DBG*) 429in [no_rv,no_dmd,p_in_ap] end 430end 431 432(* create the concrete thm to discharge the IS_ABS_FUN assum to ABS_CONS_MODEL *) 433(* could not prove this offline: 434 could not do totality because STRIP_PAIR/LIST_MK_PAIR are not well typed in the logic 435 could not do the ap thm because I ran out of time plus it required an induction on ZIP(apl,shl) that I could not figure out *) 436fun mk_is_abs_fun_thm ksname hname abs_fun state astate hR_defs_ unwind_thm (apl,ks_def,wfKS_ks) hd_def = 437 let val _ = dbgTools.DEN dpfx "miaft"(*DBG*) 438 val aftot = mk_abs_fun_total_thm abs_fun 439 val _ = dbgTools.DTH (dpfx^"miaft_ aftot") aftot (*DBG*) 440 val (st1,st2,ath_lem1,ath_lem2,afap) = mk_abs_fun_ap_thm state astate hR_defs_ unwind_thm (apl,ks_def,wfKS_ks) hd_def 441 val _ = dbgTools.DTH (dpfx^"miaft_ath_lem1") ath_lem1(*DBG*) 442 val _ = dbgTools.CBTH (dpfx^"miaft_ath_lem1") ath_lem1(*DBG*) 443 val _ = dbgTools.DTH (dpfx^"miaft_ath_lem2") ath_lem2 (*DBG*) 444 val _ = dbgTools.CBTH (dpfx^"miaft_ath_lem2") ath_lem2 (*DBG*) 445 val _ = dbgTools.DTH (dpfx^"miaft_ afap1") afap (*DBG*) 446 val iafjf = (fn _ => let val afap = REWRITE_RULE [GSYM hd_def] afap (* FIXME: do I need the rewr? it's already in terms of af *) 447 val _ = dbgTools.DTH (dpfx^"miaft_ afap2") afap (*DBG*) 448 val ciafd = (mk_conc_is_abs_fun_def st1 st2 state astate abs_fun ks_def) 449 val _ = dbgTools.DTH (dpfx^"miaft_ ciafd") ciafd (*DBG*) 450 val iaf = CONV_RULE (DEPTH_CONV PETA_CONV) (* combine aftot and afap into iaf*) 451 (REWRITE_RULE [GSYM hd_def] (REWRITE_RULE [CONJ aftot afap] ciafd)) 452 val _ = dbgTools.DTH (dpfx^"miaft_ iaf") iaf (*DBG*) 453 in iaf end) 454 val ((p_ty,st_ty),ast_ty) = (get_types ksname,type_of astate) 455 val e_var = inst [alpha |-> st_ty] envTools.env_tm 456 val iaf = mk_lthm (fn _ => (mk_forall(e_var,list_mk_comb(inst [alpha|->p_ty,beta|->st_ty,gamma|->ast_ty] is_abs_fun_tm, 457 [ksname,e_var,hname])), 458 iafjf)) iafjf 459 val _ = dbgTools.DTH (dpfx^"miaft_iaf") iaf (*DBG*) 460 val _ = dbgTools.CBTH (dpfx^"miaft_iaf") iaf (*DBG*) 461 val _ = dbgTools.DEX dpfx "miaft"(*DBG*) 462 in (ath_lem1,ath_lem2,iaf) end 463 464(* discharge, online, the assumptions to ABS_CONS_MODEL *) 465(* note enveq thm requires that both env and aenv be empty: this is true for instance if mf was originally in CTL*/LTL/CTL etc. *) 466(* FIXME: split this so that we can discharge the non-mf_assums once in one func, and discharge mf_assums again and again for each mf, 467 thus saving time, since iaf is at the moment expensive to compute but does not change with mf *) 468fun mk_abs_cons_thm mf (apl,ks_def,wfKS_ks) env aenv hd_def iaf_ vm = 469 let val _ = dbgTools.DEN dpfx "mact"(*DBG*) 470 val _ = profTools.bgt (dpfx^"mact")(*PRF*) 471 val mf_assums = mk_abs_cons_mf_thms mf (apl,ks_def,wfKS_ks) vm 472 val (p_ty,s_ty) = get_types (lhs(concl ks_def)) 473 val (hnc,args) = dest_comb(lhs(snd(strip_forall(concl hd_def)))) 474 val Qvar = mk_var("Q",stringLib.string_ty) 475 val svar = mk_var("s",s_ty) 476 val as_ty = snd(dest_prod(type_of args)) 477 val asvar = mk_var("sh",as_ty) 478 val glenveq = list_mk_forall([Qvar,svar,asvar], 479 mk_imp(mk_comb(hnc,mk_pair(svar,asvar)), 480 mk_imp(list_mk_comb(inst [alpha|->as_ty] pred_setSyntax.in_tm,[asvar,mk_comb(aenv,Qvar)]), 481 list_mk_comb(inst [alpha|->s_ty] pred_setSyntax.in_tm,[svar,mk_comb(env,Qvar)])))) 482 val _ = dbgTools.CBTM (dpfx^"mact_glenveq") glenveq (*DBG*) 483 (*``(!Q s sh. (^hnc) (s,sh) ==> sh IN (^aenv) Q ==> s IN (^env) Q)``*) 484 val jfenveq = (fn _ => (prove(glenveq, SIMP_TAC std_ss [EMPTY_ENV_def,NOT_IN_EMPTY]))) 485 val enveq = mk_lthm (fn _ => (glenveq,jfenveq)) jfenveq 486 val _ = lazyTools.testlz (dpfx^"mact_enveq") jfenveq enveq 487 val _ = dbgTools.DTM (dpfx^"mact_ env") env (*DBG*) 488 val _ = dbgTools.DTY (dpfx^"mact_ env") (type_of env) (*DBG*) 489 val _ = dbgTools.DTH (dpfx^"mact_ iaf_") iaf_ (*DBG*) 490 val iaf = ISPEC env iaf_ 491 val ast_ty = get_astate_ty hnc 492 val jfact = (fn _ => (List.foldl (fn (mpth,th) => MATCH_MP th mpth) 493 (ISPECL [mf,hnc,lhs(concl(ks_def)),env,aenv] ABS_CONS_MODEL) 494 ([wfKS_ks]@mf_assums@[iaf,enveq]))) 495 val glact = let val (vl,bod) = strip_forall (concl ABS_CONS_MODEL) 496 val (imps,bod2) = strip_imp bod 497 val conc = mk_imp(last imps,bod2) 498 val instf = (inst (mk_subst ([ks_p_ty,ks_s_ty,ks_as_ty])([p_ty,s_ty,ast_ty]))) 499 in subst (mk_subst (List.map instf vl) 500 [mf,hnc,lhs(concl(ks_def)),env,aenv]) (instf conc) end 501 val act = mk_lthm (fn _ => (glact,jfact)) jfact 502 val _ = dbgTools.DTH (dpfx^"mact_act") act (*DBG*) 503 val _ = lazyTools.testlz (dpfx^"mact_act") jfact act 504 val _ = profTools.ent (dpfx^"mact")(*PRF*) 505 val _ = dbgTools.DEX dpfx "mact"(*DBG*) 506 in act end 507 508(* ASSERT: t must be a QBF *) 509(* transforms input QBF to pure propositional formula using |- (?x. P x) = P T \/ P F and |- (!x. P x) = P F /\ P T *) 510fun elim_quant t = 511if is_exists t then let val (v,t') = dest_exists t 512 in mk_disj(elim_quant (subst [v |-> ``T``] t'),elim_quant (subst [v |-> ``F``] t')) end 513else if is_forall t then let val (v,t') = dest_forall t 514 in mk_conj(elim_quant (subst [v |-> ``T``] t'),elim_quant (subst [v |-> ``F``] t')) end 515else if is_neg t then mk_neg (elim_quant(dest_neg t)) 516else if is_conj t then mk_conj(elim_quant(fst(dest_conj t)),elim_quant(snd(dest_conj t))) 517else if is_disj t then mk_disj(elim_quant(fst(dest_disj t)),elim_quant(snd(dest_disj t))) 518else if is_eq t then mk_eq(elim_quant(fst(dest_eq t)),elim_quant(snd(dest_eq t))) 519else if is_imp t then mk_imp(elim_quant(fst(dest_imp t)),elim_quant(snd(dest_imp t))) 520else t 521 522fun mlval tm = if tm=T then true else if tm=F then false else raise Match 523 524fun mk_ass vm red res = bdd.assignment (ListPair.map (fn (v,c) => (Binarymap.find(vm,term_to_string2 v),mlval c)) (red,res)) 525 526(* check whether abstract counterexample atr has concrete counterpart upto nth state of the abstract counterexample trace*) 527(* FIXME: amba_ahb example spends a lot of time here (ctl_grant_always). is ap collapse not working? *) 528fun check_ace' atr I1 RTm(*T1*) state Ric astate h n = 529 if (n=0) then SOME [] else 530 let 531 val _ = dbgTools.DEN dpfx "ca'"(*DBG*) 532 val state' = mk_primed_state state 533 val _ = dbgTools.DTM (dpfx^"ca'_state'") state'(*DBG*) 534 val (st,st') = (strip_pair state,strip_pair state') 535 val s = List.map term_to_string2 st 536 val ace_states = atr 537 val _ = List.app (dbgTools.DTM (dpfx^"ca'_ace_states")) ace_states (*DBG*) 538 val ast = pairSyntax.strip_pair astate 539 val _ = dbgTools.DTM (dpfx^"ca'_astate") astate(*DBG*) 540 val cce_states = List.tabulate(n,fn i => pairSyntax.list_mk_pair(List.map (fn v => mk_bool_var(v^"_"^(Int.toString i))) s)) 541 val _ = List.app (dbgTools.DTM (dpfx^"ca'_cce_states")) cce_states (*DBG*) 542 val vm = getVarmap h 543 val _ = List.app (fn (k,v) => (dbgTools.DST (dpfx^"ca'_vm_k: "^k); (*DBG*) 544 dbgTools.DNM (dpfx^"ca'_vm_v: ") v)) (*DBG*) 545 (Binarymap.listItems vm) (*DBG*) 546 val _ = dbgTools.DNM (dpfx^"ca'_bdd_getVarnum") (bdd.getVarnum())(*DBG*) 547 val vm' = fst(List.foldl (fn (v,(bm,n)) => let val vs = term_to_string v 548 in if isSome (Binarymap.peek(bm,vs)) 549 then (bm,n) 550 else (Binarymap.insert(bm,vs,n),n+1) end) 551 (vm, listmax(List.map snd (Binarymap.listItems vm))+1) 552 (List.concat (List.map free_vars cce_states))) 553 val _ = List.app (fn (k,v) => (dbgTools.DST (dpfx^"ca'_vm'_k: "^k); (*DBG*) 554 dbgTools.DNM (dpfx^"ca'_vm'_v: ") v)) (*DBG*) 555 (Binarymap.listItems vm') (*DBG*) 556 val _ = if (Binarymap.numItems vm' > bdd.getVarnum()) then bdd.setVarnum (Binarymap.numItems vm') else () 557 val Ib = getBdd(t2tb vm I1) (*FIXME : this is constructed again and again. *) 558 (* val init_f = subst (mk_subst st (strip_pair(List.hd cce_states))) I1*) 559 val init_f = bdd2cnf vm' (bdd_replace vm' Ib (mk_subst st (strip_pair(List.hd cce_states)))) 560 val _ = dbgTools.DTM (dpfx^"ca'_init_f") init_f(*DBG*) 561 (*val R1 = (if Ric then list_mk_conj else list_mk_disj) (List.map snd T1) *) 562 val Rb = getBdd(Binarymap.find(RTm,".")) 563 (*val trans_f = if (n=1) then T (* special casing because list_mk_conj [] crashes *) 564 else (list_mk_conj (List.map (fn(stn,stn') => 565 subst ((mk_subst st (strip_pair stn))@(mk_subst st' (strip_pair stn'))) 566 R1) (List.tl(ListPair.zip(T::cce_states,cce_states)))))*) 567 val trans_f = if (n=1) then T (* special casing because list_mk_conj [] crashes *) 568 else (list_mk_conj (List.map (fn(stn,stn') => 569 bdd2cnf vm' (bdd_replace vm' Rb ((mk_subst st (strip_pair stn)) @ 570 (mk_subst st' (strip_pair stn'))))) 571 (List.tl(ListPair.zip(T::cce_states,cce_states))))) 572 val _ = dbgTools.DTM (dpfx^"ca'_trans_f") trans_f(*DBG*) 573 val hb = getBdd h 574 val abs_f = list_mk_conj(List.map (fn (astc,cst) => subst (mk_subst st (strip_pair cst)) 575 (bdd2cnf vm' (bdd.restrict hb (mk_ass vm ast (strip_pair astc)) ))) 576 (ListPair.zip(ace_states,cce_states))) 577 val _ = dbgTools.DTM (dpfx^"ca'_abs_f") abs_f(*DBG*) 578 579 (*FIXME: ideally I should generate a DIMACS file directly from the bdd's and have SAT call the file *) 580 (* accoding to Sofiene Tahar, this kind of file-based interface quickly becomes a performance bottleneck 581 if you make lots of calls. 582 This will be an issue if I am going to do SAT-based predicate abstraction *) 583 val satth = if is_F init_f orelse is_F trans_f orelse is_F abs_f 584 then NONE (*FIXME: fix TRUTH below so we can recover a concrete trace from it*) 585 else if is_T init_f andalso is_T trans_f andalso is_T abs_f then SOME TRUTH 586 else let val f = if is_T init_f (* making sure T does not end up in f which is supposed to be in cnf *) 587 then if is_T trans_f then abs_f 588 else if is_T abs_f then trans_f else list_mk_conj [trans_f,abs_f] 589 else if is_T trans_f then if is_T abs_f then init_f else list_mk_conj [init_f,abs_f] 590 else if is_T abs_f then list_mk_conj [init_f,trans_f] else list_mk_conj [init_f,trans_f,abs_f] 591 val _ = dbgTools.DTM (dpfx^"ca'_f") f(*DBG*) 592 val _ = dbgTools.CBTM (dpfx^"ca'_f") f(*DBG*) 593 (*val cnf = defCNF.DEF_CNF_CONV f*) 594 val cnf = f 595 val _ = dbgTools.DST (dpfx^"ca'_h1") (*DBG*) 596 in SOME (SAT_PROVE (mk_neg cnf) handle HolSatLib.SAT_cex th => th) end 597 val _ = dbgTools.DST (dpfx^"ca'_h2") (*DBG*) 598 val ctr = if isSome satth andalso is_imp (concl (valOf satth))(* return concrete trace if one was found else NONE *) 599 then let val l = strip_conj(land(concl (valOf satth))) 600 val bm = List.foldl (fn (v,bm) => if (is_neg v) then Binarymap.insert(bm,dest_neg v,F) 601 else Binarymap.insert(bm,v,T)) (Binarymap.mkDict Term.compare) 602 (snd(List.partition 603 (fn v => 604 let val vs = (*term_to_string*) (if is_neg v then dest_neg v else v) 605 in is_genvar vs (*(String.size vs >= 10) andalso 606 (String.compare(String.substring(vs,0,10),"%%genvar%%")=EQUAL)*) end) l)) 607 val _ = List.app (fn (k,v) => (dbgTools.DTM (dpfx^"ca'_bm_k:") k; (*DBG*) 608 dbgTools.DTM (dpfx^"ca'_bm_v:") v)) (*DBG*) 609 (Binarymap.listItems bm) (*DBG*) 610 val cce = List.map (fn stp => (* NotFound can happen if a conc var is in state but not in I1 and R1 *) 611 let val l = pairSyntax.strip_pair stp 612 in pairSyntax.list_mk_pair (List.map (fn v => Binarymap.find(bm,v) 613 handle NotFound => F) l) end) 614 cce_states 615 in SOME cce end 616 else NONE 617 val _ = dbgTools.DNM (dpfx^"ca'_ctrsz") (if isSome ctr then List.length (valOf ctr) else ~1) (*DBG*) 618 val _ = dbgTools.DEX dpfx "ca'"(*DBG*) 619 in ctr end 620 621(* call check_ace' for increasing n until non-SAT happens then return the greatest (i.e. previous) SAT-able path *) 622fun check_ace'' atr I1 T1 state Ric astate h n = 623 let 624 val _ = dbgTools.DEN dpfx "ca''"(*DBG*) 625 val _ = dbgTools.DNM (dpfx^"ca''_n") n (*DBG*) 626 val ctr = check_ace' atr I1 T1 state Ric astate h n 627 val res = if (isSome ctr) then let val ctr' = check_ace'' atr I1 T1 state Ric astate h (n+1) 628 in if (isSome ctr') then ctr' else ctr end 629 else ctr 630 val _ = dbgTools.DEX dpfx "ca''"(*DBG*) 631 in res end 632 633(* check whether abstract counterexample atr has concrete counterpart *) 634(* if yes return concrete counterpart else return concrete counterpart upto (not including) the state that fails satisfiability *) 635(* to check if full counterexample was discovered we can compare the length of the returned counterexample with atr *) 636(* atr is output from get_ce. FIXME thmfy ctr *) 637fun check_ace atr I1 T1 state Ric astate h = 638 let val _ = dbgTools.DEN dpfx "ca"(*DBG*) 639 val atrsz = List.length atr 640 val _ = dbgTools.DNM (dpfx^"ca_atrsz") atrsz(*DBG*) 641 val ctr = check_ace' atr I1 T1 state Ric astate h atrsz (* check if there is a full concrete counterexample *) 642 val ctr' = if (isSome ctr) then (dbgTools.DST (dpfx^"crt_ca_conc") (*DBG*); ctr) 643 else check_ace'' atr I1 T1 state Ric astate h 1 (* if not then find longest concrete prefix *) 644 val _ = dbgTools.DEX dpfx "ca"(*DBG*) 645 in ctr' end 646 647fun contract_vm vl tb = List.foldl (fn (v,tb) => BddFreevarsContractVarmap v tb) tb vl 648 649(* h as returned by mk_abs_fun. ctr as returned by check_ace, atr as returned by find_trace1 650 as_1 is abstract state to be refined. as_2 is the state after as_1 in the ace. h^-1 is inverse of h. ast is symbolic abstract state 651 compute bad = <"."> h^-1(as_2) /\ h^-1(as_1) 652 i.e. bad \subseteq as_1 and all states in bad and no other in h^-1(as_1) have a transition to h^-1(as_2) 653 compute dead = h^-1(as_1)\bad i.e. all other states in h^-1(as_1) 654 fially n is just the index of as_1 *) 655(* FIXME: can we do without requiring the BDD of M.R? *) 656fun ref_abs atr ctr state RTm astate h = 657 let val _ = dbgTools.DEN dpfx "ra"(*DBG*) 658 val as1 = pairSyntax.strip_pair(List.nth(atr,(List.length ctr)-1)) 659 val as2 = pairSyntax.strip_pair(List.nth(atr,(List.length ctr))) 660 val ast = strip_pair astate 661 val vm = getVarmap h 662 fun s2res vm st vt = ListPair.zip(List.map (fn v => BddVar true vm v) st, 663 List.map (fn v => BddCon (Term.compare(v,T)=EQUAL) vm) vt) 664 val cS1 = BddRestrict (s2res vm ast as1) h (* h^-1(as_1) *) 665 val cS2 = BddRestrict (s2res vm ast as2) h (* h^-1(as_2) *) 666 val st = pairSyntax.strip_pair state 667 val s = List.map term_to_string2 st 668 val st' = List.map mk_primed_bool_var s 669 val s2s' = List.map (fn(v,v') => (BddVar true vm v,BddVar true vm v')) (ListPair.zip(st,st')) 670 val bad = BddOp(bdd.And,cS1,BddAppex st' (bdd.And, BddExtendVarmap vm (Binarymap.find(RTm,".")), 671 (BddReplace s2s' cS2))) 672 val dead = (BddOp(bdd.And,cS1,BddNot bad)) 673 val n = List.foldl (fn (v,n) => if Term.compare(v,T)=EQUAL then 2*n else 2*n+1) 0 as1 674 val _ = dbgTools.DEX dpfx "ra"(*DBG*) 675 in (n,as1,dead,bad) end 676 677fun absCheck_aux I1 ITdf T1 RTm Ric state (apl,ks_def,wfKS_ks) astate hd_def af aksname ath_lem1 ath_lem2 iaf 678 env aenv Ree k (nf,mf) (aksinfo,abs_aks) mu_ic_snd vm (aapl,apsubs) = 679 let 680 val _ = dbgTools.DEN dpfx "aca"(*DBG*) 681 val _ = profTools.bgt (dpfx^"aca") (*PRF*) 682 val _ = profTools.bgt (dpfx^"aca_mak") (*PRF*) 683 val aksname = if isSome aksname then SOME (valOf(aksname)^"'") 684 else SOME ((despace (term_to_string (lhs(concl ks_def))))^"_aks") (*avoid overwriting prev defs*) 685 val (aI1,aT1,aItb,(abpl,aks_def,wfKS_aks,aRTm)) = (* first aks is passed in by absCheck; 686 refined ones are created here *) 687 if isSome aksinfo then valOf aksinfo 688 else mk_abs_ks I1 ITdf RTm state astate Ric af (valOf aksname) (apl,ks_def,wfKS_ks) hd_def 689 val aenv = inst [alpha |-> type_of astate] envTools.empty_env_tm 690 val _ = dbgTools.DTB (dpfx^"aca_af") af 691 val _ = dbgTools.DBD (dpfx^"aca_af_bdd") (getBdd af) 692 val _ = dbgTools.DTB (dpfx^"aca_aItb") aItb 693 val _ = dbgTools.DBD (dpfx^"aca_aItb_bdd") (getBdd aItb) 694 val _ = dbgTools.DTB (dpfx^"aca_hd_aRTm") (snd (hd (Binarymap.listItems aRTm))) 695 val _ = dbgTools.DBD (dpfx^"aca_hd_aRTm_bdd") (getBdd (snd (hd (Binarymap.listItems aRTm)))) 696 val _ = dbgTools.DTB (dpfx^"aca_hd_RTm") (snd (hd (Binarymap.listItems RTm))) 697 val _ = dbgTools.DBD (dpfx^"aca_hd_RTm_bdd") (getBdd (snd (hd (Binarymap.listItems RTm)))) 698 val _ = profTools.ent (dpfx^"aca_mak") (*PRF*) 699 val (state',astate',st) = (mk_primed_state state,mk_primed_state astate,strip_pair state) 700 val _ = profTools.bgt (dpfx^"aca_maat") (*PRF*) 701 val abs_aks = if isSome abs_aks then valOf abs_aks 702 else mk_abs_aks_thm state astate af state' astate' st hd_def ks_def aks_def 703 val _ = profTools.ent (dpfx^"aca_maat") (*PRF*) 704 val vm'' = PrimitiveBddRules.getVarmap (Binarymap.find(aRTm,".")) 705 val _ = profTools.ent (dpfx^"aca") (*PRF*) 706 (*FIXME: Since the model has changed (after refinement), we can't pass muCheck the thms from the previous checking; 707 can something from mu_ic_snc be salvaged however? *) 708 val ((tb,tbth,ace),mu_ic) = muCheck.muCheck Ree aI1 aT1 astate vm'' Ric (ref NONE) ((SOME af), SOME aItb) 709 {ks=SOME (abpl,aks_def,wfKS_aks,aRTm,NONE),th=NONE} (nf,mf) 710 val _ = profTools.bgt (dpfx^"aca") (*PRF*) 711 val _ = profTools.bgt (dpfx^"aca_mact") (*PRF*) 712 val cth = if (not (isSome ace)) (* final success theorem *) 713 then let val acm = mk_abs_cons_thm mf (apl,ks_def,wfKS_ks) env aenv hd_def iaf vm 714 val _ = dbgTools.DTH (dpfx^"aca_abs_aks") abs_aks (*DBG*) 715 val _ = dbgTools.DTH (dpfx^"aca_tbth") (valOf tbth) (*DBG*) 716 val _ = dbgTools.CBTH (dpfx^"aca_abs_aks") abs_aks (*DBG*) 717 val _ = dbgTools.CBTH (dpfx^"aca_acm") acm (*DBG*) 718 val _ = dbgTools.CBTH (dpfx^"aca_tbth") (valOf tbth) (*DBG*) 719 in SOME (MP acm (PURE_ONCE_REWRITE_RULE [abs_aks] (valOf tbth))) end 720 else NONE 721 val _ = profTools.ent (dpfx^"aca_mact") (*PRF*) 722 val _ = profTools.bgt (dpfx^"aca_chkace") (*PRF*) 723 val _ = if (isSome cth) then dbgTools.DTH (dpfx^"aca_cth") (valOf cth) else () (*DBG*) 724 val cce = if (isSome ace) (* concrete counter example (or prefix if ace was spurious) *) 725 then check_ace (valOf ace) I1 RTm state Ric astate af 726 else NONE 727 val _ = profTools.ent (dpfx^"aca_chkace") (*PRF*) 728 val _ = profTools.ent (dpfx^"aca") (*PRF*) 729 in if (isSome cth) 730 then (dbgTools.DEX dpfx "aca"(*DBG*); ((tb,cth,NONE),#th(mu_ic))) (* success *) 731 else 732 if (List.length (valOf cce)) = (List.length (valOf ace)) 733 then (dbgTools.DEX dpfx "aca"(*DBG*); ((tb,NONE,cce),#th(mu_ic))) (*failure*) 734 else let val _ = profTools.bgt (dpfx^"aca") (*PRF*) 735 val _ = profTools.bgt (dpfx^"aca_ref") (*PRF*) 736 val (idx,as1,dead,bad) = ref_abs (valOf ace) (valOf cce) state RTm astate af (* refine *) 737 val (af,ath_lem1,astate,hd_def,iaf)= 738 mk_ref_abs_fun af state astate ks_def ath_lem1 ath_lem2 hd_def idx as1 dead bad k 739 val _ = profTools.ent (dpfx^"aca_ref") (*PRF*) 740 val _ = profTools.ent (dpfx^"aca") (*PRF*) 741 in absCheck_aux I1 ITdf T1 RTm Ric state (apl,ks_def,wfKS_ks) astate 742 hd_def af aksname ath_lem1 ath_lem2 iaf env aenv Ree (k+1) (nf,mf) (NONE,NONE) (#th(mu_ic)) vm 743 (aapl,apsubs) end 744 end 745 746(* property independent theorems and data that needs to be initialised only once per model *) 747fun init_abs I1 T1 state Ric vm (aapl,apsubs) ksname (ic,cc) = 748 let 749 val _ = dbgTools.DEN dpfx "ia" (*DBG*) 750 val _ = profTools.bgt (dpfx^"ia") (*PRF*) 751 val _ = profTools.bgt (dpfx^"ia_mck") (*PRF*) 752 val (apl,ks_def,wfKS_ks,RTm,ITdf) = if isSome (#ks(#mu(ic))) then valOf (#ks(#mu(ic))) 753 else mk_wfKS I1 T1 NONE state vm Ric aapl NONE ksname 754 val _ = profTools.ent (dpfx^"ia_mck") (*PRF*) 755 val _ = profTools.bgt (dpfx^"ia_maf") (*PRF*) 756 val hname = SOME ((despace (term_to_string (lhs(concl ks_def))))^"_af") (* so ctl and mu names don't collide *) 757 val ((astate,af),state,env,aenv,Ree,k,unwind_thm,hR_defs_,hd_def) = 758 if isSome (#abs_df(cc)) then valOf(#abs_df(cc)) 759 else let val (astate,unwind_thm,hR_defs_,hd_def,af) = mk_abs_fun (valOf aapl) vm state hname 760 val env = inst [alpha |-> type_of state] envTools.empty_env_tm 761 val aenv = inst [alpha |-> type_of astate] envTools.empty_env_tm 762 val Ree = Array.fromList [] 763 val k = Real.round(Math.pow(2.0,Real.fromInt(List.length (strip_pair astate)))) 764 in ((astate,af),state,env,aenv,Ree,k,unwind_thm,hR_defs_,hd_def) end 765 val _ = profTools.ent (dpfx^"ia_maf") (*PRF*) 766 val _ = profTools.bgt (dpfx^"ia_mak") (*PRF*) 767 val aksname = SOME ((despace (term_to_string (lhs(concl ks_def))))^"_aks") (* so ctl and mu names don't collide *) 768 val (aI1,aT1,aItb,(abpl,aks_def,wfKS_aks,aRTm)) = 769 if isSome (#ks(ic)) then valOf (#ks(ic)) 770 else mk_abs_ks I1 ITdf RTm state astate Ric af (valOf aksname) (apl,ks_def,wfKS_ks) hd_def 771 val _ = profTools.ent (dpfx^"ia_mak") (*PRF*) 772 val _ = profTools.bgt (dpfx^"ia_maat") (*PRF*) 773 val (state',astate',st) = (mk_primed_state state,mk_primed_state astate,strip_pair state) 774 val abs_aks = mk_abs_aks_thm state astate af state' astate' st hd_def ks_def aks_def 775 val _ = profTools.ent (dpfx^"ia_maat") (*PRF*) 776 val _ = profTools.bgt (dpfx^"ia_miaf") (*PRF*) 777 val ksname = lhs(concl ks_def) 778 val hnc = rator(lhs(snd(strip_forall(concl hd_def)))) 779 val (ath_lem1,ath_lem2,iaf) = mk_is_abs_fun_thm ksname hnc af state astate hR_defs_ unwind_thm (apl,ks_def,wfKS_ks) hd_def 780 val _ = profTools.ent (dpfx^"ia_miaf") (*PRF*) 781 val _ = profTools.ent (dpfx^"ia") (*PRF*) 782 val _ = dbgTools.DEX dpfx "ia" (*DBG*) 783 in ((apl,ks_def,wfKS_ks,RTm,ITdf),(aI1,aT1,aItb,(abpl,aks_def,wfKS_aks,aRTm)), 784 ((astate,af),state,env,aenv,Ree,k,unwind_thm,hR_defs_,hd_def), 785 (ath_lem1,ath_lem2,abs_aks,iaf)) end 786 787(* so far the res tells us that the collapsed (i.e. propositional subterms folded into single AP's ) property holds in the concrete ks*) 788(* now prove that non-collapsed property holds as well (since that is what the user should see) *) 789fun finalise (apl,ks_def,wfKS_ks,ITdf) apsubs state mf (*msa*) (tb,th,tr) = 790 if isSome th 791 then let val _ = dbgTools.DEN dpfx "fin"(*DBG*) 792 val _ = profTools.bgt (dpfx^"fin") (*PRF*) 793 val subs = List.map dest_subst apsubs 794 val faps = HOLset.addList(HOLset.empty Term.compare,find_APs mf) 795 val fsubs = List.filter (((curry HOLset.member) faps) o snd) subs 796 val (gmf,aap) = ListPair.unzip fsubs 797 val ksname = lhs(concl ks_def) 798 val _ = dbgTools.DTM (dpfx^"fin_ksname") ksname(*DBG*) 799 val (p_ty,s_ty) = get_types ksname 800 val is_prop = List.map (prove_is_prop p_ty) gmf 801 val _ = List.app (dbgTools.DTH (dpfx^"fin_is_prop")) is_prop (*DBG*) 802 val _ = dbgTools.CBTHL (dpfx^"fin_is_prop") is_prop (*DBG*) 803 val lm = CONV_RULE (LHS_CONV (lzGEN_PALPHA_CONV state)) (INST_TYPE [alpha|->s_ty] (SPEC T FORALL_SIMP)) 804 val _ = dbgTools.DTH (dpfx^"fin_lm") lm(*DBG*) 805 val _ = dbgTools.CBTH (dpfx^"fin_lm") lm (*DBG*) 806 val apth = MATCH_MP AP_SUBST_MODEL wfKS_ks 807 val _ = dbgTools.DTH (dpfx^"fin_apth") apth(*DBG*) 808 val apth = CONV_RULE (STRIP_QUANT_CONV (RAND_CONV (LAND_CONV (lzGEN_PALPHA_CONV state)))) apth 809 val _ = dbgTools.DTH (dpfx^"fin_apth2") apth(*DBG*) 810 val _ = dbgTools.CBTH (dpfx^"fin_apth") apth (*DBG*) 811 val th = valOf th 812 val _ = dbgTools.DTH (dpfx^"fin_th") th(*DBG*) 813 val env = el 3 (snd(strip_comb(snd(strip_forall(concl th))))) 814 val _ = dbgTools.DTM (dpfx^"fin_env") env(*DBG*) 815 val msthl = List.map (fn th => MATCH_MP (CONV_RULE lzFORALL_IMP_CONV (ISPECL [state,ksname] th)) wfKS_ks) 816 [MU_SAT_T,MU_SAT_F,MU_SAT_NEG,MU_SAT_CONJ,MU_SAT_DISJ,MU_SAT_AP] 817 val _ = List.app (dbgTools.DTH (dpfx^"fin_msthl")) msthl (*DBG*) 818 val _ = dbgTools.CBTHL (dpfx^"fin_msthl") msthl (*DBG*) 819 val Lth = mk_Lth ks_def 820 val _ = dbgTools.DTH (dpfx^"fin_Lth") Lth(*DBG*) 821 val _ = dbgTools.CBTH (dpfx^"fin_Lth") Lth (*DBG*) 822 val _ = dbgTools.CBTH (dpfx^"fin_wfKS_ks") wfKS_ks (*DBG*) 823 val _ = dbgTools.CBTM (dpfx^"fin_state") state (*DBG*) 824 val res = List.foldl (fn ((ip,(g,ap)),th) => 825 let val mf = hd(snd(strip_comb(snd(strip_forall(concl th))))) 826 val _ = dbgTools.DTM (dpfx^"fin_mf") mf(*DBG*) 827 val _ = dbgTools.CBTM (dpfx^"fin_mf") mf (*DBG*) 828 val _ = dbgTools.DTM (dpfx^"fin_g") g(*DBG*) 829 val _ = dbgTools.CBTM (dpfx^"fin_g") g (*DBG*) 830 val _ = dbgTools.DTM (dpfx^"fin_ap") ap(*DBG*) 831 val _ = dbgTools.CBTM (dpfx^"fin_ap") ap (*DBG*) 832 val _ = dbgTools.DTM (dpfx^"fin_env") env(*DBG*) 833 val _ = dbgTools.CBTM (dpfx^"fin_env") env (*DBG*) 834 val sapth = ISPECL [mf,g,rand ap,env] apth 835 val _ = dbgTools.DTH (dpfx^"fin_sapth") sapth(*DBG*) 836 val _ = dbgTools.CBTH (dpfx^"fin_sapth") sapth (*DBG*) 837 val _ = dbgTools.CBTM (dpfx^"fin_apeqgl") (land (rand (concl sapth))) (*DBG*) 838 val apeq = EQT_ELIM ((REWRITE_CONV (Lth::wfKS_ks::msthl) 839 THENC (DEPTH_CONV PBETA_CONV) 840 THENC REWRITE_CONV [lm]) (land (rand (concl sapth)))) 841 val _ = dbgTools.DTH (dpfx^"fin_apeq") apeq(*DBG*) 842 val _ = dbgTools.CBTH (dpfx^"fin_apeq") apeq (*DBG*) 843 val sapth2 = MATCH_MP (MATCH_MP sapth ip) apeq 844 val _ = dbgTools.DTH (dpfx^"fin_sapth2") sapth2(*DBG*) 845 val _ = dbgTools.CBTH (dpfx^"fin_sapth2") sapth2 (*DBG*) 846 in REWRITE_RULE [sapth2,AP_SUBST_def] th end) 847 th (ListPair.zip(is_prop,fsubs)) 848 val _ = dbgTools.DTH (dpfx^"fin_res") res(*DBG*) 849 val restb = tb 850 val _ = profTools.ent (dpfx^"fin") (*PRF*) 851 val _ = dbgTools.DEX dpfx "fin" (*DBG*) 852 in (restb,SOME res,tr) end 853 else (tb,th,tr) 854 855(* given concrete model M and a formula f, returns M |= f where the model checking has been done on an abstracted version of M *) 856(* NOTE: this abstraction framework is only for universal properties; the second test for no aapl checks if hct.maA returned apl=NONE *) 857(* this function just computes the init data (or picks it from the ic); the real action takes place in absCheck_aux *) 858fun absCheck I1 T1 state Ric vm ksname (ic:internalCacheTools.abs_ic,cc:internalCacheTools.common_ic) (nf,mf) (aapl,apsubs) = 859 let 860 val _ = dbgTools.DEN dpfx "ac"(*DBG*) 861 val res = if is_existential mf orelse (not (isSome aapl)) 862 then let val _ = dbgTools.DST (dpfx^"ac_ No abstraction") (*DBG*) 863 val _ = profTools.bgt (dpfx^"ac_no")(*PRF*) 864 val (apl,ks_def,wfKS_ks,RTm,ITdf) = if isSome (#ks(#mu(ic))) then valOf (#ks(#mu(ic))) 865 else mk_wfKS I1 T1 NONE state vm Ric NONE NONE ksname 866 val _ = profTools.ent (dpfx^"ac_no") (*PRF*) 867 val (res,mu_ic) = muCheck (Array.fromList []) I1 T1 state vm Ric (ref NONE) (NONE,NONE) 868 {ks=SOME (apl,ks_def,wfKS_ks,RTm,ITdf),th= #th(#mu(ic))} (nf,mf) 869 val _ = dbgTools.DST (dpfx^"ac_ absCheck done (without abstraction)") (*DBG*) 870 in (res,({mth= #mth(ic),th= #th(ic),ks= #ks(ic),mu={ks= #ks(mu_ic),th= #th(mu_ic)}},cc)) end 871 else let val _ = dbgTools.DST (dpfx^"ac_ Abstracting") (*DBG*) 872 val _ = profTools.bgt (dpfx^"ac_yes")(*PRF*) 873 val ((apl,ks_def,wfKS_ks,RTm,ITdf),(aI1,aT1,aItb,(abpl,aks_def,wfKS_aks,aRTm)), 874 ((astate,af),state,env,aenv,Ree,k,abst_def,hR_defs_,hd_def), 875 (ath_lem1,ath_lem2,abs_aks,iaf)) = 876 if isSome (#th(ic)) 877 then (valOf(#ks(#mu(ic))),valOf(#ks(ic)),valOf(#abs_df(cc)),valOf(#th(ic))) 878 else init_abs I1 T1 state Ric vm (aapl,apsubs) ksname (ic,cc) 879 val mf2 = subst apsubs mf (*FIXME: cache the substs and use that cache somehow *) 880 val (res,mu_ic_snd) = absCheck_aux I1 ITdf T1 RTm Ric state (apl,ks_def,wfKS_ks) 881 astate hd_def af NONE ath_lem1 ath_lem2 iaf 882 env aenv Ree k (nf,mf2) 883 (SOME (aI1,aT1,aItb,(abpl,aks_def,wfKS_aks,aRTm)),SOME abs_aks) (#mth(ic)) 884 vm (aapl,apsubs) 885 val res = finalise (apl,ks_def,wfKS_ks,ITdf) apsubs state mf2 res 886 val _ = profTools.ent (dpfx^"ac_yes") (*PRF*) 887 val _ = dbgTools.DST (dpfx^"ac_ absCheck done (with abstraction)") (*DBG*) 888 in (res, 889 ({mu={ks=SOME (apl,ks_def,wfKS_ks,RTm,ITdf),th= #th(#mu(ic))}, 890 mth= mu_ic_snd, 891 ks=SOME(aI1,aT1,aItb,(abpl,aks_def,wfKS_aks,aRTm)), 892 th=SOME(ath_lem1,ath_lem2,abs_aks,iaf)}, 893 {abs_df=SOME((astate,af),state,env,aenv,Ree,k,abst_def,hR_defs_,hd_def)})) 894 end 895 val _ = dbgTools.DEX dpfx "ac" (*DBG*) 896 in res end 897 898end 899end 900