examples/HolCheck/cacheTools.sml

402 fun cache_add depth rvnm2ix env (nf,mf) mfo ce rsc rvty ithml (githms as [_,_,T_I,F_I,_,_,_,_,_,_,_,_,_,_,_,_,_,_])
411         val cekey = if irv then mk_comb(rvtm, (fromMLstring((fromHOLstring(rand mf))^(int_to_string depth)))) else mf
412         (*mu_RV (type_of state) (fromMLstring((fromHOLstring(rand mf))^(int_to_string depth))) else mf*)
422     (* reverse scoping for RV's is more complicated, so it is quicker to just cache on name+depth (a la de Bruijn) to tell them apart *)
475                         (*val _ = print_rsc rsc "RV cache_add depth"*)
650 fun mk_cache_aux ee rvnm2ix env (nf,mf) mfo ce rscope depth rvty githms state seth msp guid tysimps p_ty
660                       val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty []
669                       val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty []
677          | "RV" =>let val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty []
686          | "AP" =>let val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty []
697                                         ce rscope depth rvty githms state seth msp guid tysimps p_ty cons
698                        val (pt,(ce2,rsc2,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce1 rsc rvty
707                                         rscope depth rvty githms state seth msp guid tysimps p_ty cons
710                                         rsc depth rvty githms state seth msp guid tysimps p_ty cons
711                        val (pt,(ce3,rsc3,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce2 (rcs_merge rsc rsc2)
727                                        rscope depth rvty githms state seth msp guid tysimps p_ty cons
730                                        rsc depth rvty githms state seth msp guid tysimps p_ty cons
731                       val (pt,(ce3,rsc3,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce2 (rcs_merge rsc rsc2)
741                                             rscope depth rvty githms state seth msp guid tysimps p_ty cons
742                            val (pt,(ce2,rsc2,ithm,ab))=cache_add depth rvnm2ix env (nf,mf) mfo ce1 rsc rvty
752                                         rscope depth rvty githms state seth msp guid tysimps p_ty cons
753                        val (pt,(ce2,rsc2,ithm,ab))=cache_add depth rvnm2ix env (nf,mf) mfo ce1 rsc rvty
761          | "mu" => let val (ptr,(ce0,rsc,ithm,abthm)) = cache_add (depth+1)
762                                                                  ((fromHOLstring(List.hd args),depth)::rvnm2ix)
766                             mk_cache_aux ee ((fromHOLstring(List.hd args),depth)::rvnm2ix)
767                                          env (nf,(List.last args)) (List.last argso) ce0 rscope (depth+1)
773                           cache_add depth rvnm2ix env (nf,mf) mfo ce1
774                                     (Vector.mapi (fn (i,v) => if (i=depth) then
788          | "nu" => let val (ptr,(ce0,rsc,ithm,abthm)) = cache_add (depth+1)
789                                                              ((fromHOLstring(List.hd args),depth)::rvnm2ix)
793                             mk_cache_aux ee ((fromHOLstring(List.hd args),depth)::rvnm2ix)
794                                          env (nf,(List.last args)) (List.last argso) ce0 rscope (depth+1)
800                            cache_add depth rvnm2ix env (nf,mf) mfo ce1
801                                      (Vector.mapi (fn (i,v) => if (i=depth) then