Refactor construction of type templates

coord-e · coord-e · commit 3f431a8bdd3b · 2025-10-24T16:53:42.000+09:00
diff --git a/src/analyze.rs b/src/analyze.rs
@@ -123,22 +123,12 @@ pub struct Analyzer<'tcx> {
     enum_defs: Rc<RefCell<HashMap<DefId, rty::EnumDatatypeDef>>>,
 }
 
-impl<'tcx> crate::refine::TemplateTypeGenerator<'tcx> for Analyzer<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-
+impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> {
     fn register_template<V>(&mut self, tmpl: rty::Template<V>) -> rty::RefinedType<V> {
         tmpl.into_refined_type(|pred_sig| self.generate_pred_var(pred_sig))
     }
 }
 
-impl<'tcx> crate::refine::UnrefinedTypeGenerator<'tcx> for Analyzer<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-}
-
 impl<'tcx> Analyzer<'tcx> {
     pub fn generate_pred_var(&mut self, sig: chc::PredSig) -> chc::PredVarId {
         self.system
diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
@@ -14,7 +14,7 @@ use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{
     self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx,
-    TemplateTypeGenerator, UnrefinedTypeGenerator, Var,
+    TypeBuilder, Var,
 };
 use crate::rty::{
     self, ClauseBuilderExt as _, ClauseScope as _, ShiftExistential as _, Subtyping as _,
@@ -222,9 +222,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                         let rty_args: IndexVec<_, _> = args
                             .types()
                             .map(|ty| {
-                                self.ctx
-                                    .build_template_ty_with_scope(&self.env)
-                                    .refined_ty(ty)
+                                TypeBuilder::new(self.tcx)
+                                    .for_template(&mut self.ctx)
+                                    .with_scope(&self.env)
+                                    .build_refined(ty)
                             })
                             .collect();
                         for (field_pty, mut variant_rty) in
@@ -237,7 +238,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                             self.ctx.extend_clauses(cs);
                         }
 
-                        let sort_args: Vec<_> = rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
+                        let sort_args: Vec<_> =
+                            rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
                         let ty = rty::EnumType::new(ty_sym.clone(), rty_args).into();
 
                         let mut builder = PlaceTypeBuilder::default();
@@ -433,7 +435,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let func_ty = match func.const_fn_def() {
             // TODO: move this to well-known defs?
             Some((def_id, args)) if self.is_box_new(def_id) => {
-                let inner_ty = self.ctx.build_template_ty().ty(args.type_at(0)).vacuous();
+                let inner_ty = TypeBuilder::new(self.tcx)
+                    .for_template(&mut self.ctx)
+                    .build(args.type_at(0))
+                    .vacuous();
                 let param = rty::RefinedType::unrefined(inner_ty.clone());
                 let ret_term =
                     chc::Term::box_(chc::Term::var(rty::FunctionParamIdx::from(0_usize)));
@@ -444,7 +449,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 rty::FunctionType::new([param].into_iter().collect(), ret).into()
             }
             Some((def_id, args)) if self.is_mem_swap(def_id) => {
-                let inner_ty = self.ctx.unrefined_ty(args.type_at(0)).vacuous();
+                let inner_ty = TypeBuilder::new(self.tcx).build(args.type_at(0)).vacuous();
                 let param1 =
                     rty::RefinedType::unrefined(rty::PointerType::mut_to(inner_ty.clone()).into());
                 let param2 =
@@ -531,7 +536,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     fn add_prophecy_var(&mut self, statement_index: usize, ty: mir_ty::Ty<'tcx>) {
-        let ty = self.ctx.unrefined_ty(ty);
+        let ty = TypeBuilder::new(self.tcx).build(ty);
         let temp_var = self.env.push_temp_var(ty.vacuous());
         self.prophecy_vars.insert(statement_index, temp_var);
         tracing::debug!(stmt_idx = %statement_index, temp_var = ?temp_var, "add_prophecy_var");
@@ -552,7 +557,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         referent: mir::Place<'tcx>,
         prophecy_ty: mir_ty::Ty<'tcx>,
     ) -> rty::RefinedType<Var> {
-        let prophecy_ty = self.ctx.unrefined_ty(prophecy_ty);
+        let prophecy_ty = TypeBuilder::new(self.tcx).build(prophecy_ty);
         let prophecy = self.env.push_temp_var(prophecy_ty.vacuous());
         let place = self.elaborate_place_for_borrow(&referent);
         self.env.borrow_place(place, prophecy).into()
@@ -664,10 +669,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             }
 
             let decl = self.local_decls[destination].clone();
-            let rty = self
-                .ctx
-                .build_template_ty_with_scope(&self.env)
-                .refined_ty(decl.ty);
+            let rty = TypeBuilder::new(self.tcx)
+                .for_template(&mut self.ctx)
+                .with_scope(&self.env)
+                .build_refined(decl.ty);
             self.type_call(func.clone(), args.clone().into_iter().map(|a| a.node), &rty);
             self.bind_local(destination, rty);
         }
@@ -738,9 +743,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     #[tracing::instrument(skip(self))]
     fn ret_template(&mut self) -> rty::RefinedType<Var> {
         let ret_ty = self.body.local_decls[mir::RETURN_PLACE].ty;
-        self.ctx
-            .build_template_ty_with_scope(&self.env)
-            .refined_ty(ret_ty)
+        TypeBuilder::new(self.tcx)
+            .for_template(&mut self.ctx)
+            .with_scope(&self.env)
+            .build_refined(ret_ty)
     }
 
     // TODO: remove this
diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
@@ -11,7 +11,7 @@ use rustc_span::symbol::Ident;
 use crate::analyze;
 use crate::annot::{self, AnnotFormula, AnnotParser, ResolverExt as _};
 use crate::chc;
-use crate::refine::{self, TemplateTypeGenerator, UnrefinedTypeGenerator};
+use crate::refine::{self, TypeBuilder};
 use crate::rty::{self, ClauseBuilderExt as _};
 
 /// An implementation of local crate analysis.
@@ -132,13 +132,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
         let mut param_resolver = analyze::annot::ParamResolver::default();
         for (input_ident, input_ty) in self.tcx.fn_arg_names(def_id).iter().zip(sig.inputs()) {
-            let input_ty = self.ctx.unrefined_ty(*input_ty);
+            let input_ty = TypeBuilder::new(self.tcx).build(*input_ty);
             param_resolver.push_param(input_ident.name, input_ty.to_sort());
         }
 
         let mut require_annot = self.extract_require_annot(&param_resolver, def_id);
         let mut ensure_annot = {
-            let output_ty = self.ctx.unrefined_ty(sig.output());
+            let output_ty = TypeBuilder::new(self.tcx).build(sig.output());
             let resolver = annot::StackedResolver::default()
                 .resolver(analyze::annot::ResultResolver::new(output_ty.to_sort()))
                 .resolver((&param_resolver).map(rty::RefinedTypeVar::Free));
@@ -175,7 +175,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             self.trusted.insert(def_id);
         }
 
-        let mut builder = self.ctx.build_function_template_ty(sig);
+        let mut builder = TypeBuilder::new(self.tcx).for_function_template(&mut self.ctx, sig);
         if let Some(AnnotFormula::Formula(require)) = require_annot {
             let formula = require.map_var(|idx| {
                 if idx.index() == sig.inputs().len() - 1 {
@@ -303,8 +303,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
                             // the subst doesn't contain refinements, so it's OK to take ty only
                             // after substitution
-                            let mut field_rty =
-                                rty::RefinedType::unrefined(self.ctx.unrefined_ty(field_ty));
+                            let mut field_rty = rty::RefinedType::unrefined(
+                                TypeBuilder::new(self.tcx).build(field_ty),
+                            );
                             field_rty.subst_ty_params(&subst);
                             field_rty.ty
                         })
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
@@ -11,7 +11,7 @@ use rustc_span::def_id::LocalDefId;
 use crate::analyze;
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
-use crate::refine::{BasicBlockType, TemplateTypeGenerator};
+use crate::refine::{BasicBlockType, TypeBuilder};
 use crate::rty;
 
 /// An implementation of the typing of local definitions.
@@ -306,7 +306,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             }
             // function return type is basic block return type
             let ret_ty = self.body.local_decls[mir::RETURN_PLACE].ty;
-            let rty = self.ctx.basic_block_template_ty(live_locals, ret_ty);
+            let rty = TypeBuilder::new(self.tcx)
+                .for_template(&mut self.ctx)
+                .build_basic_block(live_locals, ret_ty);
             self.ctx.register_basic_block_ty(self.local_def_id, bb, rty);
         }
     }
diff --git a/src/refine.rs b/src/refine.rs
@@ -8,7 +8,7 @@
 //! module and remove this one.
 
 mod template;
-pub use template::{TemplateScope, TemplateTypeGenerator, UnrefinedTypeGenerator};
+pub use template::{TemplateRegistry, TemplateScope, TypeBuilder};
 
 mod basic_block;
 pub use basic_block::BasicBlockType;
diff --git a/src/refine/env.rs b/src/refine/env.rs
@@ -558,7 +558,8 @@ impl rty::ClauseScope for Env {
     }
 }
 
-impl refine::TemplateScope<Var> for Env {
+impl refine::TemplateScope for Env {
+    type Var = Var;
     fn build_template(&self) -> rty::TemplateBuilder<Var> {
         let mut builder = rty::TemplateBuilder::default();
         for (v, sort) in self.dependencies() {
diff --git a/src/refine/template.rs b/src/refine/template.rs

Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,7 @@ use rustc_span::def_id::LocalDefId;`
`11`	`11`	`use crate::analyze;`
`12`	`12`	`use crate::chc;`
`13`	`13`	`use crate::pretty::PrettyDisplayExt as _;`
`14`		`-use crate::refine::{BasicBlockType, TemplateTypeGenerator};`
	`14`	`+use crate::refine::{BasicBlockType, TypeBuilder};`
`15`	`15`	`use crate::rty;`
`16`	`16`
`17`	`17`	`/// An implementation of the typing of local definitions.`
`@@ -306,7 +306,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {`
`306`	`306`	`}`
`307`	`307`	`// function return type is basic block return type`
`308`	`308`	`let ret_ty = self.body.local_decls[mir::RETURN_PLACE].ty;`
`309`		`- let rty = self.ctx.basic_block_template_ty(live_locals, ret_ty);`
	`309`	`+ let rty = TypeBuilder::new(self.tcx)`
	`310`	`+ .for_template(&mut self.ctx)`
	`311`	`+ .build_basic_block(live_locals, ret_ty);`
`310`	`312`	`self.ctx.register_basic_block_ty(self.local_def_id, bb, rty);`
`311`	`313`	`}`
`312`	`314`	`}`
Original file line number	Diff line number	Diff line change
`@@ -558,7 +558,8 @@ impl rty::ClauseScope for Env {`
`558`	`558`	`}`
`559`	`559`	`}`
`560`	`560`
`561`		`-impl refine::TemplateScope<Var> for Env {`
	`561`	`+impl refine::TemplateScope for Env {`
	`562`	`+ type Var = Var;`
`562`	`563`	`fn build_template(&self) -> rty::TemplateBuilder<Var> {`
`563`	`564`	`let mut builder = rty::TemplateBuilder::default();`
`564`	`565`	`for (v, sort) in self.dependencies() {`