sva-formula 0.7.13

Laws in t and f: the normal form, the rule table, and the observations a law answers without sampling
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

// Concern: declares the Env a term reads node and parameter types through | Non-concern: holding a graph (sva-engine) | IO: (NodeId) -> Ty

use crate::ty::Ty;

#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct NodeId(pub u32);

#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct ParamId(pub u32);

/// Total on both lookups: the graph resolves every ref before a closed form reaches this crate, so a
/// missing id is the caller's contract violation, not a case to type around.
pub trait Env {
    fn node(&self, id: NodeId) -> Ty;
    fn param(&self, id: ParamId) -> Ty;
}