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