sva-formula 0.7.18

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
17
18
19
20
21
22

// 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

use crate::through::{Opaque, Reads};
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;

    /// What a ref reads as through the forms the caller holds, where it holds them.
    fn reads(&self) -> &dyn Reads {
        &Opaque
    }
}