Skip to main content

find_refined_type

aver::codegen::common

Function find_refined_type 

Source 
pub fn find_refined_type<'a>(
    ctx: &'a CodegenContext,
    name: &str,
) -> Option<&'a RefinedTypeDecl>
Expand description

Issue #128: do all of a law’s givens carry a singleton domain?

Resolve a (possibly bare) type name to its [RefinedTypeDecl] in ctx.proof_ir.refined_types. The IR is keyed by canonical name (bare for entry types, Module.Name for module types); callers see whatever the AST node carried (Expr::RecordCreate { type_name: "Natural" } is bare, obj.ty() on a stamped expression can be either).

Resolution order:

  1. Direct lookup (covers exact-canonical hits and bare entry types).
  2. If no direct hit, walk ctx.modules for a type def with this bare name and try Module.Name keys until one resolves.

Returns None if no match — consistent with the previous HashMap::get semantics. Two modules declaring the same bare name (A.Natural + B.Natural with distinct predicates) each get their own canonical slot now; a direct-canonical-key lookup disambiguates correctly, and a bare-name lookup resolves to the first module that owns the name (typechecker’s cross_module_same_named_types_do_not_merge rejects mixed usage upstream, so the order-dependence is observed only when a project carries one such refined type as actually-used and the other as dead-code in deps).