Lines Matching defs:ix
106 val apnm2ix =fst(Vector.foldl (fn(nm,(bm,ix)) => (Binarymap.insert(bm,term_to_string2(getTerm(nm)),ix),ix+1))
111 val _ =Binarymap.app (fn(nm,ix)=> dbgTools.DST (dpfx^ ("("^nm^","^(int_to_string ix)^")"))) apnm2ix(*DBG*)*)
167 fun mk_rv_tb ee (_,_,_,_,ix,_,_,_,_,_) mf sth =
172 val _ = dbgTools.DST (dpfx^ (int_to_string ix)) (*DBG*)
173 val _ = dbgTools.DST (dpfx^ " ix\n") (*DBG*)
176 val _ = dbgTools.DTM (dpfx^ (getTerm (snd(Array.sub(ee,ix))))) (*DBG*)
178 val res = BddEqMp sth (snd(Array.sub(ee,ix)))
183 fun mk_rv_spec_thm msr seth sel msreq ie ee state (tb,gth,sth,env,ix,rsc,ithm,abthm,_,_) dp mf =
197 val th = if (Int.compare(ix,dp)=EQUAL
198 andalso (Vector.sub(rsc,ix)>0)) (*i.e.current bnd var top level fv filt by >0 test*)
295 let val (tb,gth,sth,env,ix,rsc,ithm,abthm,ado_subthm,ado_eqthm) = !cch
299 val _ = dbgTools.DST (dpfx^ (Int.toString ix)) val _ = dbgTools.DST (dpfx^ " ix\n") (*DBG*)
570 val ix = (Array.length ee) - qd (* index of current bv in ee and rv_thms arrays *)
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))
602 val _ = if (Option.isSome (!ce)) andalso ix=0 then ce := SOME (itr::(Option.valOf (!ce))) else ()
603 (*val _ = if (Option.isSome (!ce)) andalso ix=0 then (*DBG*)
609 val prevbdd = snd(Array.sub(ee,ix))
683 val _ = Array.update(ee,ix,(bv,itr))