litex-lang 0.9.65-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

use crate::obj::Obj;
use std::collections::HashMap;

/// Turn user-written parameter names into prefixed storage names (e.g. `x` -> `__x`).
pub fn mangled_fn_param_names(user_written_names: &[String], prefix: &str) -> Vec<String> {
    user_written_names
        .iter()
        .map(|u| format!("{}{}", prefix, u))
        .collect()
}

/// `user_name -> Identifier(mangled)` for `inst_obj` / `inst_*` substitution.
pub fn fn_param_substitution_map(
    user_written_names: &[String],
    mangled_names: &[String],
) -> HashMap<String, Obj> {
    debug_assert_eq!(user_written_names.len(), mangled_names.len());
    let mut map = HashMap::with_capacity(user_written_names.len());
    for (u, m) in user_written_names.iter().zip(mangled_names.iter()) {
        map.insert(u.clone(), m.clone().into());
    }
    map
}

/// Build mangled names and substitution map; `prefix` is usually `DEFAULT_MANGLED_FN_PARAM_PREFIX`.
pub fn mangled_fn_param_binding(
    user_written_names: &[String],
    prefix: &str,
) -> (Vec<String>, HashMap<String, Obj>) {
    let mangled = mangled_fn_param_names(user_written_names, prefix);
    let map = fn_param_substitution_map(user_written_names, &mangled);
    (mangled, map)
}