examples/HolCheck/muCheck.sml

90 fun mk_gen_rv_thms mf ksname state rvl ie wfKS_ks =
183 fun mk_rv_spec_thm msr seth sel msreq ie ee state (tb,gth,sth,env,ix,rsc,ithm,abthm,_,_) dp mf =
186         (*val _ = dbgTools.DTM (dpfx^  ie)      val _ = dbgTools.DST (dpfx^  " ie \n") (*DBG*)*)
193         val _ = dbgTools.DTM (dpfx^  ie)  val _ = dbgTools.DST (dpfx^  " ie\n") (*DBG*)
204                            val _ = dbgTools.DTH (dpfx^  (ISPECL [ie,fromMLstring v] msr))
209                             val _ = dbgTools.DTH (dpfx^  (eval_env ie ie bv seth [])) (*DBG*)
211                       in SYM (CONV_RULE(RHS_CONV(PURE_ONCE_REWRITE_CONV [eval_env ie ie bv state seth sel []]))
212                                        (ISPECL [ie,bv] msr)) end
217 (* in case an mf is an RV, getting the spec thm is more than just SPEC'ing the gth with the ie *)
218 fun get_spec_thm ie spec_func gth mf =
225                       (*val _ = dbgTools.DST (dpfx^  "not RV \n")  val _ = dbgTools.DST (dpfx^ _type (type_of ie))
226                        val _ = dbgTools.DST (dpfx^  " ie type\n") (*DBG*)
228                       in SPEC ie gth end
294 fun cache_get cch ie tb_func gth_func dp nodes mf seth sel state =
304         (*val _ = with_flag (show_types,true) dbgTools.DTM (dpfx^  ie)  val _ = dbgTools.DST (dpfx^  " ie\n") (*DBG*)
306      val res = if (Term.compare(env,ie)=EQUAL)
321                             val sth = get_spec_thm ie gth_func (Option.valOf gth) mf (* could be an RV *)
330                             val sth = ISPEC ie gth
344                         val sth1 = get_spec_thm ie gth_func (Option.valOf gth) mf (* could be an RV *)
347                         val sithm = mk_spec_inv_thm ithm nodes env ie mf seth
357                         val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth1 val _ = upd_cch_env cch ie
363                         val sth = get_spec_thm ie gth_func (Option.valOf gth) mf (* could be an RV *)
365                         val _ = upd_cch_tb cch tb val _ = upd_cch_sth cch sth val _ = upd_cch_env cch ie
369                         val sth = if (is_RV mf) then gth else ISPEC ie gth
374                         val _ = upd_cch_gth cch gth val _ = upd_cch_env cch ie
394 fun muCheck_aux ((_,(msa,absf,ksname),_,_,_),(seth,sel,state,ie)) mf vm dp (muAP cch) =
396         val tb = cache_get cch ie (mk_ap_tb vm absf) (mk_gen_ap_thm ksname state msa) dp [] mf seth sel state
399   | muCheck_aux ((_,_,(msr,_,msreq,ee),_,_),(seth,sel,state,ie)) mf vm dp (muRV cch) =
401         val tb = cache_get cch ie (mk_rv_tb ee (!cch)) (mk_rv_spec_thm msr seth sel msreq ie ee state (!cch) dp) dp []
405   | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muAnd(cch,(f1,f2))) =
408         val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
409             (fn mf => GEN ``e:^(ty_antiq(type_of ie))``
410              (ISPECL [``e:^(ty_antiq(type_of ie))``,cab1nm,cab2nm]
413   | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muOr(cch,(f1,f2))) =
416         val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
417             (fn mf => GEN ``e:^(ty_antiq(type_of ie))``
418              (ISPECL [``e:^(ty_antiq(type_of ie))``,cab1nm,cab2nm]
421   | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muNot(cch,f1)) =
424         val tb = cache_get cch ie (NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm)
427   | muCheck_aux ((msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muTR cch) =
428         cache_get cch ie (mk_con_tb true vm) (fn mf => (List.nth(msp,0))) dp [] mf seth sel state
429   | muCheck_aux ((msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muFL cch) =
430         cache_get cch ie (mk_con_tb false vm) (fn mf => (List.nth(msp,1))) dp [] mf seth sel state
431   | muCheck_aux (args as (_,_,_,(_,Tth,(dmdth,_),_,_),_),(seth,sel,state,ie)) mf vm dp (muDIAMOND(cch,(act,f1))) =
434          val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act false (List.last(snd(strip_comb mf)))
438   | muCheck_aux (args as (_,_,_,(_,Tth,(_,boxth),_,_),_),(seth,sel,state,ie)) mf vm dp (muBOX(cch,(act,f1))) =
441          val tb = cache_get cch ie (ModalExp (args,(seth,sel,state,ie)) act true (List.last(snd(strip_comb mf)))
445   | muCheck_aux (args,(seth,sel,state,ie)) mf vm dp (fpmu(bvch,cch,f1)) =
449         val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon false vm) vm
453   | muCheck_aux (args,(seth,sel,state,ie)) mf vm dp (fpnu(bvch,cch,f1)) =
457         val tb = cache_get cch ie (FixExp (args,(seth,sel,state,ie)) [rvnm,cabthmnm] (BddCon true vm) vm
462 and NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm mf sth =
465         val tb = BddNot (muCheck_aux (args,(seth,sel,state,ie)) mf1 vm dp f1)
476 and BinExp (args,(seth,sel,state,ie)) opr [t1,t2] vm (f1,f2) dp abthm mf opthm =
480         val b1 = muCheck_aux (args,(seth,sel,state,ie)) t1 vm dp f1
482         val b2 = muCheck_aux (args,(seth,sel,state,ie)) t2 vm dp f2
496 and ModalExp (args as (_,_,_,(RTm,_,_,sp,s2sp),_),(seth,sel,state,ie))  actnm isbox t2 vm f1 dp abthm mf sth =
499         val tb1 = muCheck_aux (args,(seth,sel,state,ie)) t2 vm dp f1
515            (seth,sel,state,ie)) [t1,t2] initbdd vm (bvch,_,f1) dp abthm cabthm mf _ =
534         val _ = dbgTools.DTM (dpfx^  ie)  val _ = dbgTools.DST (dpfx^  " ie\n") (*DBG*)*)
538                   andalso (not (Term.compare(numSyntax.zero_tm,List.last(snd(strip_comb(snd(dest_comb ie)))))=EQUAL))
563         val ie1 = list_mk_comb(eus,[ie,t1,initset])
565         val ie2 = list_mk_comb(eus,[ie,t1,mk_fp numSyntax.zero_tm])
567         val new_rv_thm = SYM (MP (ISPECL [t2,ksname,ie,t1,state,initset,numSyntax.zero_tm] MS_FP_INIT) wfKS_ks)
573                 then Array.update(ee,ix,(bv,BddEqMp (SYM(MP (ISPECL [t2,ksname,ie,t1,initset,state] init_thm) wfKS_ks))
575             else Array.update(ee,ix,(bv,BddEqMp (SYM(MP (ISPECL [t2,ksname,ie,t1,state] init_thm) wfKS_ks)) initbdd))
577             wfKS_ks ie t1 initset seth imf_t2 ess Ss eus adogeneqthm initsubth numSyntax.zero_tm) else NONE
585               val eeqthm  = if sqd then mk_ado_pre_sub_thm ado ado_subthm t2 ksname ie1 eeq imf_thms abthm wfKS_ks ie t1
598               val itrthm = (ISPECL [t2,ksname,ie,t1,state,initset,n] MS_FP)
637                                             val _ = dbgTools.DTM (dpfx^ ie) val _ = dbgTools.DST (dpfx^" ADO ie\n")(*DBG*)
641                                                            (SPEC (fst (dest_env ie))
648                                             val sabbrev_thm = ISPECL [t2,ksname,ie,n,t1,initset] abbrev_thm
654                                else MP (PURE_REWRITE_RULE [SYM abthm] (ISPECL [t2,ksname,ie,n,t1] abbrev_thm))
665                                    val ado_eqthm' = CONV_RULE(RHS_CONV(REWRITE_CONV[MP(ISPECL[t2,ksname,ie,t1] bigthm)
672                                        imf_thms abthm wfKS_ks ie t1 initset (rator (getTerm prevbdd)) seth
681                            val ie3 = list_mk_comb(eus,[ie,t1,mk_fp(mk_comb(``SUC``,n))])
684                            val _ = dbgTools.CBTML (dpfx^"fe_rv_thm_tml") [t2,ie,initset,t1,n]
686                            val rv_thm = SYM (SPECL [t2,ie,initset,t1,n] rvtt)
758         val ie =  if (List.null rvl) then (``EMPTY_ENV:^(ty_antiq(env_ty))``) else mk_env rvl state
760         val (msr,(seth,sel),msreq) = mk_gen_rv_thms mf ksname state rvl ie wfKS_ks
770         val (mfml,imf_thms,frv_thms) = mk_cache ee ie (nf,mf) mf qd githms state (seth,sel) msp
786     in (ie,(msr,seth,sel,msreq,ee2),mfml,imf_thms,frv_thms,qd,sqd,mf) end
804         val (ie,(msr,seth,sel,msreq,ee2),mfml,imf_thms,frv_thms,qd,sqd,mf) =
818         (ks_def,mf,seth,sel,ie,mfml,frv_thms,ce))
908 fun checkResult tb mf ks_def (I1,Itb,ITdf) state ie vm =
940                                                                (ISPECL [mf,ksname,ie] MU_MODEL_SAT_def))
958         val (ic,init_stuff,(ks_def,mf,seth,sel,ie,mfml,frv_thms,ce')) = init I1 T1 state vm Ric ce (nf,mf) ee absf ic
959         val tb = muCheck_aux (init_stuff,(seth,sel,state,ie)) mf vm ((Array.length ee)-1) mfml
963                             else checkResult res_tb mf ks_def (I1,Itb,#5(valOf(#ks(ic)))) state ie vm