Skip to main content

sva_formula/
env.rs

1// Concern: declares the Env a term reads node and parameter types through | Non-concern: holding a graph (sva-engine) | IO: (NodeId) -> Ty
2
3use crate::ty::Ty;
4
5#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
6pub struct NodeId(pub u32);
7
8#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
9pub struct ParamId(pub u32);
10
11/// Total on both lookups: the graph resolves every ref before a closed form reaches this crate, so a
12/// missing id is the caller's contract violation, not a case to type around.
13pub trait Env {
14    fn node(&self, id: NodeId) -> Ty;
15    fn param(&self, id: ParamId) -> Ty;
16}