Skip to main content

prune_lang/interp/solver/
common.rs

1use super::*;
2
3pub trait PrimSolver {
4    fn check_sat(
5        &mut self,
6        prims: &[(Prim, Vec<AtomVal<IdentCtx>>)],
7    ) -> Option<HashMap<IdentCtx, LitVal>>;
8}
9
10pub fn infer_type(prims: &[(Prim, Vec<AtomVal<IdentCtx>>)]) -> HashMap<IdentCtx, LitType> {
11    let mut map = HashMap::new();
12
13    for (prim, args) in prims.iter() {
14        for (arg, typ) in args.iter().zip(prim.get_typ().iter()) {
15            match arg {
16                Term::Var(var) => {
17                    if let Some(res) = map.get(var) {
18                        assert_eq!(*res, *typ);
19                    } else {
20                        map.insert(*var, *typ);
21                    }
22                }
23                Term::Lit(lit) => {
24                    assert_eq!(lit.get_typ(), *typ);
25                }
26                Term::Cons(_, _) => unreachable!(),
27            }
28        }
29    }
30
31    map
32}