Skip to main content

litex/runtime/
runtime_instantiate_have_fn_forall.rs

1// Normalize ForallFact from have fn / have fn by induc before storage.
2//
3// The same source name (e.g. x) can appear as different free-param tags: Forall (~1), FnSet (~5)
4// from the fn header parse, or Induc (~7) in nested induc case facts. Stored foralls should use
5// one ForallFreeParamObj per quantified name from the header. We build name -> ForallFreeParamObj,
6// then inst_fact(..., ParamObjType::FnSet). inst_obj substitutes FnSet, Forall, and Induc atoms when
7// the name is in that map and ctx is FnSet (see runtime_instantiate_obj.rs).
8
9use crate::prelude::*;
10use std::collections::HashMap;
11
12impl Runtime {
13    pub fn inst_have_fn_forall_fact_for_store(
14        &self,
15        forall_fact: ForallFact,
16    ) -> Result<Fact, RuntimeError> {
17        let param_to_arg_map = have_fn_forall_store_binding_map(&forall_fact);
18        let fact: Fact = forall_fact.into();
19        self.inst_fact(&fact, &param_to_arg_map, ParamObjType::FnSet, None)
20    }
21}
22
23fn have_fn_forall_store_binding_map(forall_fact: &ForallFact) -> HashMap<String, Obj> {
24    let mut param_to_arg_map = HashMap::new();
25    for group in forall_fact.params_def_with_type.groups.iter() {
26        for name in group.params.iter() {
27            param_to_arg_map.insert(name.clone(), ForallFreeParamObj::new(name.clone()).into());
28        }
29    }
30    param_to_arg_map
31}