oxilean_std/hashmap/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4#![allow(clippy::items_after_test_module)]
5
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7use oxilean_kernel::{
8    BinderInfo as HmBI, Declaration as HmDecl, Expr as HmExpr, Level as HmLevel, Name as HmName,
9};
10
11use super::types::{
12    AssocMap, BiMap, FreqMap, IndexedMap, IntervalMap, LruMap, MultiMap, PersistentMap, StackMap,
13};
14
15/// Build HashMap type in the environment.
16pub fn build_hashmap_env(env: &mut Environment) -> Result<(), String> {
17    let type1 = Expr::Sort(Level::succ(Level::zero()));
18    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
19    let hashmap_ty = Expr::Pi(
20        BinderInfo::Default,
21        Name::str("K"),
22        Box::new(type1.clone()),
23        Box::new(Expr::Pi(
24            BinderInfo::Default,
25            Name::str("V"),
26            Box::new(type1.clone()),
27            Box::new(type2.clone()),
28        )),
29    );
30    env.add(Declaration::Axiom {
31        name: Name::str("HashMap"),
32        univ_params: vec![],
33        ty: hashmap_ty,
34    })
35    .map_err(|e| e.to_string())?;
36    let empty_ty = Expr::Pi(
37        BinderInfo::Implicit,
38        Name::str("K"),
39        Box::new(type1.clone()),
40        Box::new(Expr::Pi(
41            BinderInfo::Implicit,
42            Name::str("V"),
43            Box::new(type1.clone()),
44            Box::new(Expr::App(
45                Box::new(Expr::App(
46                    Box::new(Expr::Const(Name::str("HashMap"), vec![])),
47                    Box::new(Expr::BVar(1)),
48                )),
49                Box::new(Expr::BVar(0)),
50            )),
51        )),
52    );
53    env.add(Declaration::Axiom {
54        name: Name::str("HashMap.empty"),
55        univ_params: vec![],
56        ty: empty_ty,
57    })
58    .map_err(|e| e.to_string())?;
59    let insert_ty = Expr::Pi(
60        BinderInfo::Implicit,
61        Name::str("K"),
62        Box::new(type1.clone()),
63        Box::new(Expr::Pi(
64            BinderInfo::Implicit,
65            Name::str("V"),
66            Box::new(type1.clone()),
67            Box::new(Expr::Pi(
68                BinderInfo::Default,
69                Name::str("k"),
70                Box::new(Expr::BVar(1)),
71                Box::new(Expr::Pi(
72                    BinderInfo::Default,
73                    Name::str("v"),
74                    Box::new(Expr::BVar(1)),
75                    Box::new(Expr::Pi(
76                        BinderInfo::Default,
77                        Name::str("m"),
78                        Box::new(Expr::App(
79                            Box::new(Expr::App(
80                                Box::new(Expr::Const(Name::str("HashMap"), vec![])),
81                                Box::new(Expr::BVar(3)),
82                            )),
83                            Box::new(Expr::BVar(2)),
84                        )),
85                        Box::new(Expr::App(
86                            Box::new(Expr::App(
87                                Box::new(Expr::Const(Name::str("HashMap"), vec![])),
88                                Box::new(Expr::BVar(4)),
89                            )),
90                            Box::new(Expr::BVar(3)),
91                        )),
92                    )),
93                )),
94            )),
95        )),
96    );
97    env.add(Declaration::Axiom {
98        name: Name::str("HashMap.insert"),
99        univ_params: vec![],
100        ty: insert_ty,
101    })
102    .map_err(|e| e.to_string())?;
103    let lookup_ty = Expr::Pi(
104        BinderInfo::Implicit,
105        Name::str("K"),
106        Box::new(type1.clone()),
107        Box::new(Expr::Pi(
108            BinderInfo::Implicit,
109            Name::str("V"),
110            Box::new(type1.clone()),
111            Box::new(Expr::Pi(
112                BinderInfo::Default,
113                Name::str("k"),
114                Box::new(Expr::BVar(1)),
115                Box::new(Expr::Pi(
116                    BinderInfo::Default,
117                    Name::str("m"),
118                    Box::new(Expr::App(
119                        Box::new(Expr::App(
120                            Box::new(Expr::Const(Name::str("HashMap"), vec![])),
121                            Box::new(Expr::BVar(2)),
122                        )),
123                        Box::new(Expr::BVar(1)),
124                    )),
125                    Box::new(Expr::App(
126                        Box::new(Expr::Const(Name::str("Option"), vec![])),
127                        Box::new(Expr::BVar(2)),
128                    )),
129                )),
130            )),
131        )),
132    );
133    env.add(Declaration::Axiom {
134        name: Name::str("HashMap.lookup"),
135        univ_params: vec![],
136        ty: lookup_ty,
137    })
138    .map_err(|e| e.to_string())?;
139    Ok(())
140}
141/// A map from `Name` to `Expr`, backed by an association list.
142pub type NameExprMap = AssocMap<Name, Expr>;
143/// A map from `String` to arbitrary values, backed by an association list.
144pub type StringMap<V> = AssocMap<String, V>;
145/// Build a `NameExprMap` from an iterator of `(Name, Expr)` pairs.
146pub fn name_expr_map_from_iter(iter: impl IntoIterator<Item = (Name, Expr)>) -> NameExprMap {
147    let mut map = NameExprMap::new();
148    for (k, v) in iter {
149        map.insert(k, v);
150    }
151    map
152}
153/// Build `HashMap.delete : {K V : Type} → K → HashMap K V → HashMap K V`.
154pub fn build_hashmap_delete(env: &mut Environment) -> Result<(), String> {
155    let type1 = Expr::Sort(Level::succ(Level::zero()));
156    let delete_ty = Expr::Pi(
157        BinderInfo::Implicit,
158        Name::str("K"),
159        Box::new(type1.clone()),
160        Box::new(Expr::Pi(
161            BinderInfo::Implicit,
162            Name::str("V"),
163            Box::new(type1.clone()),
164            Box::new(Expr::Pi(
165                BinderInfo::Default,
166                Name::str("k"),
167                Box::new(Expr::BVar(1)),
168                Box::new(Expr::Pi(
169                    BinderInfo::Default,
170                    Name::str("m"),
171                    Box::new(Expr::App(
172                        Box::new(Expr::App(
173                            Box::new(Expr::Const(Name::str("HashMap"), vec![])),
174                            Box::new(Expr::BVar(2)),
175                        )),
176                        Box::new(Expr::BVar(1)),
177                    )),
178                    Box::new(Expr::App(
179                        Box::new(Expr::App(
180                            Box::new(Expr::Const(Name::str("HashMap"), vec![])),
181                            Box::new(Expr::BVar(3)),
182                        )),
183                        Box::new(Expr::BVar(2)),
184                    )),
185                )),
186            )),
187        )),
188    );
189    env.add(Declaration::Axiom {
190        name: Name::str("HashMap.delete"),
191        univ_params: vec![],
192        ty: delete_ty,
193    })
194    .map_err(|e| e.to_string())
195}
196/// Build `HashMap.size : {K V : Type} → HashMap K V → Nat`.
197pub fn build_hashmap_size(env: &mut Environment) -> Result<(), String> {
198    let type1 = Expr::Sort(Level::succ(Level::zero()));
199    let size_ty = Expr::Pi(
200        BinderInfo::Implicit,
201        Name::str("K"),
202        Box::new(type1.clone()),
203        Box::new(Expr::Pi(
204            BinderInfo::Implicit,
205            Name::str("V"),
206            Box::new(type1.clone()),
207            Box::new(Expr::Pi(
208                BinderInfo::Default,
209                Name::str("m"),
210                Box::new(Expr::App(
211                    Box::new(Expr::App(
212                        Box::new(Expr::Const(Name::str("HashMap"), vec![])),
213                        Box::new(Expr::BVar(1)),
214                    )),
215                    Box::new(Expr::BVar(0)),
216                )),
217                Box::new(Expr::Const(Name::str("Nat"), vec![])),
218            )),
219        )),
220    );
221    env.add(Declaration::Axiom {
222        name: Name::str("HashMap.size"),
223        univ_params: vec![],
224        ty: size_ty,
225    })
226    .map_err(|e| e.to_string())
227}
228/// Build all HashMap operations into the environment.
229pub fn build_hashmap_extended(env: &mut Environment) -> Result<(), String> {
230    build_hashmap_env(env)?;
231    build_hashmap_delete(env)?;
232    build_hashmap_size(env)?;
233    Ok(())
234}
235/// Count entries in an AssocMap matching a predicate.
236pub fn count_matching<K: PartialEq + Clone, V: Clone>(
237    map: &AssocMap<K, V>,
238    pred: impl Fn(&K, &V) -> bool,
239) -> usize {
240    map.iter().filter(|(k, v)| pred(k, v)).count()
241}
242/// Convert a Vec of pairs into an AssocMap.
243pub fn assoc_map_from_vec<K: PartialEq + Clone, V: Clone>(pairs: Vec<(K, V)>) -> AssocMap<K, V> {
244    let mut map = AssocMap::new();
245    for (k, v) in pairs {
246        map.insert(k, v);
247    }
248    map
249}
250#[cfg(test)]
251mod tests {
252    use super::*;
253    fn setup_env() -> Environment {
254        let mut env = Environment::new();
255        let type1 = Expr::Sort(Level::succ(Level::zero()));
256        let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
257        let option_ty = Expr::Pi(
258            BinderInfo::Default,
259            Name::str("α"),
260            Box::new(type1.clone()),
261            Box::new(type2),
262        );
263        env.add(Declaration::Axiom {
264            name: Name::str("Option"),
265            univ_params: vec![],
266            ty: option_ty,
267        })
268        .expect("operation should succeed");
269        env.add(Declaration::Axiom {
270            name: Name::str("Nat"),
271            univ_params: vec![],
272            ty: type1,
273        })
274        .expect("operation should succeed");
275        env
276    }
277    #[test]
278    fn test_build_hashmap_env() {
279        let mut env = setup_env();
280        assert!(build_hashmap_env(&mut env).is_ok());
281        assert!(env.get(&Name::str("HashMap")).is_some());
282        assert!(env.get(&Name::str("HashMap.empty")).is_some());
283    }
284    #[test]
285    fn test_hashmap_insert() {
286        let mut env = setup_env();
287        build_hashmap_env(&mut env).expect("build_hashmap_env should succeed");
288        let decl = env
289            .get(&Name::str("HashMap.insert"))
290            .expect("declaration 'HashMap.insert' should exist in env");
291        assert!(matches!(decl, Declaration::Axiom { .. }));
292    }
293    #[test]
294    fn test_hashmap_lookup() {
295        let mut env = setup_env();
296        build_hashmap_env(&mut env).expect("build_hashmap_env should succeed");
297        let decl = env
298            .get(&Name::str("HashMap.lookup"))
299            .expect("declaration 'HashMap.lookup' should exist in env");
300        assert!(matches!(decl, Declaration::Axiom { .. }));
301    }
302    #[test]
303    fn test_assoc_map_insert_and_get() {
304        let mut map: AssocMap<String, u32> = AssocMap::new();
305        map.insert("a".to_string(), 1);
306        map.insert("b".to_string(), 2);
307        assert_eq!(map.get(&"a".to_string()), Some(&1));
308        assert_eq!(map.get(&"b".to_string()), Some(&2));
309        assert_eq!(map.get(&"c".to_string()), None);
310    }
311    #[test]
312    fn test_assoc_map_overwrite() {
313        let mut map: AssocMap<String, u32> = AssocMap::new();
314        map.insert("x".to_string(), 10);
315        map.insert("x".to_string(), 20);
316        assert_eq!(map.get(&"x".to_string()), Some(&20));
317        assert_eq!(map.len(), 1);
318    }
319    #[test]
320    fn test_assoc_map_remove() {
321        let mut map: AssocMap<String, u32> = AssocMap::new();
322        map.insert("a".to_string(), 1);
323        let removed = map.remove(&"a".to_string());
324        assert_eq!(removed, Some(1));
325        assert!(map.is_empty());
326    }
327    #[test]
328    fn test_assoc_map_merge() {
329        let mut m1: AssocMap<String, u32> = AssocMap::new();
330        m1.insert("a".to_string(), 1);
331        let mut m2: AssocMap<String, u32> = AssocMap::new();
332        m2.insert("b".to_string(), 2);
333        m2.insert("a".to_string(), 99);
334        m1.merge(&m2);
335        assert_eq!(m1.get(&"a".to_string()), Some(&99));
336        assert_eq!(m1.get(&"b".to_string()), Some(&2));
337    }
338    #[test]
339    fn test_assoc_map_retain() {
340        let mut map: AssocMap<String, u32> = AssocMap::new();
341        map.insert("a".to_string(), 1);
342        map.insert("b".to_string(), 2);
343        map.insert("c".to_string(), 3);
344        map.retain(|_, v| *v > 1);
345        assert_eq!(map.len(), 2);
346        assert!(!map.contains_key(&"a".to_string()));
347    }
348    #[test]
349    fn test_persistent_map_insert_get() {
350        let m0: PersistentMap<i32, &str> = PersistentMap::empty();
351        let m1 = m0.insert(1, "one");
352        let m2 = m1.insert(2, "two");
353        assert_eq!(m1.get(&1), Some(&"one"));
354        assert_eq!(m1.get(&2), None);
355        assert_eq!(m2.get(&1), Some(&"one"));
356        assert_eq!(m2.get(&2), Some(&"two"));
357    }
358    #[test]
359    fn test_persistent_map_sorted_output() {
360        let m: PersistentMap<i32, i32> = PersistentMap::empty()
361            .insert(3, 30)
362            .insert(1, 10)
363            .insert(2, 20);
364        let sorted = m.to_sorted_vec();
365        assert_eq!(sorted, vec![(1, 10), (2, 20), (3, 30)]);
366    }
367    #[test]
368    fn test_persistent_map_overwrite() {
369        let m = PersistentMap::empty().insert(1, "old").insert(1, "new");
370        assert_eq!(m.get(&1), Some(&"new"));
371        assert_eq!(m.len(), 1);
372    }
373    #[test]
374    fn test_multi_map_insert_get() {
375        let mut mm: MultiMap<String, u32> = MultiMap::new();
376        mm.insert("k".to_string(), 1);
377        mm.insert("k".to_string(), 2);
378        mm.insert("k".to_string(), 3);
379        assert_eq!(mm.get(&"k".to_string()), &[1, 2, 3]);
380        assert_eq!(mm.total_count(), 3);
381        assert_eq!(mm.key_count(), 1);
382    }
383    #[test]
384    fn test_multi_map_remove() {
385        let mut mm: MultiMap<String, u32> = MultiMap::new();
386        mm.insert("a".to_string(), 10);
387        let vals = mm.remove(&"a".to_string());
388        assert_eq!(vals, vec![10]);
389        assert!(mm.is_empty());
390    }
391    #[test]
392    fn test_name_expr_map() {
393        let nat = Expr::Const(Name::str("Nat"), vec![]);
394        let map = name_expr_map_from_iter(vec![
395            (Name::str("x"), nat.clone()),
396            (Name::str("y"), nat.clone()),
397        ]);
398        assert_eq!(map.get(&Name::str("x")), Some(&nat));
399        assert_eq!(map.len(), 2);
400    }
401    #[test]
402    fn test_build_hashmap_delete() {
403        let mut env = setup_env();
404        build_hashmap_env(&mut env).expect("build_hashmap_env should succeed");
405        assert!(build_hashmap_delete(&mut env).is_ok());
406        assert!(env.get(&Name::str("HashMap.delete")).is_some());
407    }
408    #[test]
409    fn test_build_hashmap_extended() {
410        let mut env = setup_env();
411        assert!(build_hashmap_extended(&mut env).is_ok());
412        assert!(env.get(&Name::str("HashMap.delete")).is_some());
413        assert!(env.get(&Name::str("HashMap.size")).is_some());
414    }
415    #[test]
416    fn test_assoc_map_keys_values() {
417        let mut map: AssocMap<i32, i32> = AssocMap::new();
418        map.insert(1, 10);
419        map.insert(2, 20);
420        let keys: Vec<i32> = map.keys().copied().collect();
421        let vals: Vec<i32> = map.values().copied().collect();
422        assert_eq!(keys, vec![1, 2]);
423        assert_eq!(vals, vec![10, 20]);
424    }
425    #[test]
426    fn test_bimap_insert_lookup() {
427        let mut m: BiMap<String, u32> = BiMap::new();
428        m.insert("a".to_string(), 1);
429        m.insert("b".to_string(), 2);
430        assert_eq!(m.get_by_key(&"a".to_string()), Some(&1));
431        assert_eq!(m.get_by_val(&2), Some(&"b".to_string()));
432    }
433    #[test]
434    fn test_bimap_evicts_on_collision() {
435        let mut m: BiMap<String, u32> = BiMap::new();
436        m.insert("a".to_string(), 1);
437        m.insert("b".to_string(), 1);
438        assert!(m.get_by_key(&"a".to_string()).is_none());
439    }
440    #[test]
441    fn test_lrumap_eviction() {
442        let mut m: LruMap<u32, u32> = LruMap::new(2);
443        m.insert(1, 10);
444        m.insert(2, 20);
445        m.insert(3, 30);
446        assert!(m.peek(&1).is_none());
447        assert_eq!(m.peek(&3), Some(&30));
448    }
449    #[test]
450    fn test_stackmap_shadowing() {
451        let mut m: StackMap<String, u32> = StackMap::new();
452        m.insert("x".to_string(), 1);
453        m.push_scope();
454        m.insert("x".to_string(), 2);
455        assert_eq!(m.get(&"x".to_string()), Some(&2));
456        m.pop_scope();
457        assert_eq!(m.get(&"x".to_string()), Some(&1));
458    }
459    #[test]
460    fn test_freq_map_record() {
461        let mut f: FreqMap<String> = FreqMap::new();
462        f.record("a".to_string());
463        f.record("a".to_string());
464        f.record("b".to_string());
465        assert_eq!(f.count(&"a".to_string()), 2);
466        assert_eq!(f.count(&"b".to_string()), 1);
467        assert_eq!(f.total_count(), 3);
468    }
469    #[test]
470    fn test_freq_map_most_common() {
471        let mut f: FreqMap<u32> = FreqMap::new();
472        f.record(1);
473        f.record(2);
474        f.record(2);
475        f.record(2);
476        let (k, c) = f.most_common().expect("most_common should succeed");
477        assert_eq!(*k, 2);
478        assert_eq!(c, 3);
479    }
480    #[test]
481    fn test_interval_map_query() {
482        let mut m: IntervalMap<u32, &str> = IntervalMap::new();
483        m.insert(0, 10, "a");
484        m.insert(5, 15, "b");
485        m.insert(20, 30, "c");
486        let results = m.query(&7);
487        assert_eq!(results.len(), 2);
488        assert!(results.contains(&&"a"));
489        assert!(results.contains(&&"b"));
490    }
491    #[test]
492    fn test_interval_map_no_match() {
493        let mut m: IntervalMap<u32, &str> = IntervalMap::new();
494        m.insert(0, 5, "a");
495        assert!(m.query(&10).is_empty());
496    }
497    #[test]
498    fn test_indexed_map_insert_get() {
499        let mut m: IndexedMap<String> = IndexedMap::new();
500        m.insert(0, "hello".to_string());
501        m.insert(5, "world".to_string());
502        assert_eq!(m.get(0), Some(&"hello".to_string()));
503        assert_eq!(m.get(5), Some(&"world".to_string()));
504        assert!(m.get(3).is_none());
505        assert_eq!(m.len(), 2);
506    }
507    #[test]
508    fn test_indexed_map_remove() {
509        let mut m: IndexedMap<u32> = IndexedMap::new();
510        m.insert(0, 42);
511        let old = m.remove(0);
512        assert_eq!(old, Some(42));
513        assert!(m.is_empty());
514    }
515    #[test]
516    fn test_indexed_map_iter() {
517        let mut m: IndexedMap<u32> = IndexedMap::new();
518        m.insert(0, 10);
519        m.insert(2, 30);
520        let pairs: Vec<_> = m.iter().collect();
521        assert_eq!(pairs.len(), 2);
522    }
523    #[test]
524    fn test_count_matching() {
525        let mut m: AssocMap<u32, u32> = AssocMap::new();
526        m.insert(1, 10);
527        m.insert(2, 20);
528        m.insert(3, 5);
529        assert_eq!(count_matching(&m, |_, v| *v >= 10), 2);
530    }
531    #[test]
532    fn test_assoc_map_from_vec() {
533        let m = assoc_map_from_vec(vec![("a", 1u32), ("b", 2), ("a", 99)]);
534        assert_eq!(m.get(&"a"), Some(&99));
535        assert_eq!(m.len(), 2);
536    }
537}
538/// Prop sort.
539#[allow(dead_code)]
540pub fn hm_prop() -> HmExpr {
541    HmExpr::Sort(HmLevel::zero())
542}
543/// Type₁ sort.
544#[allow(dead_code)]
545pub fn hm_type1() -> HmExpr {
546    HmExpr::Sort(HmLevel::succ(HmLevel::zero()))
547}
548/// Type₂ sort.
549#[allow(dead_code)]
550pub fn hm_type2() -> HmExpr {
551    HmExpr::Sort(HmLevel::succ(HmLevel::succ(HmLevel::zero())))
552}
553/// Named constant.
554#[allow(dead_code)]
555pub fn hm_cst(s: &str) -> HmExpr {
556    HmExpr::Const(HmName::str(s), vec![])
557}
558/// Bound variable.
559#[allow(dead_code)]
560pub fn hm_bvar(n: u32) -> HmExpr {
561    HmExpr::BVar(n)
562}
563/// Application `f a`.
564#[allow(dead_code)]
565pub fn hm_app(f: HmExpr, a: HmExpr) -> HmExpr {
566    HmExpr::App(Box::new(f), Box::new(a))
567}
568/// Application `f a b`.
569#[allow(dead_code)]
570pub fn hm_app2(f: HmExpr, a: HmExpr, b: HmExpr) -> HmExpr {
571    hm_app(hm_app(f, a), b)
572}
573/// Application `f a b c`.
574#[allow(dead_code)]
575pub fn hm_app3(f: HmExpr, a: HmExpr, b: HmExpr, c: HmExpr) -> HmExpr {
576    hm_app(hm_app2(f, a, b), c)
577}
578/// Pi binder.
579#[allow(dead_code)]
580pub fn hm_pi(bi: HmBI, name: &str, dom: HmExpr, body: HmExpr) -> HmExpr {
581    HmExpr::Pi(bi, HmName::str(name), Box::new(dom), Box::new(body))
582}
583/// Non-dependent arrow `A → B`.
584#[allow(dead_code)]
585pub fn hm_arrow(a: HmExpr, b: HmExpr) -> HmExpr {
586    hm_pi(HmBI::Default, "_", a, b)
587}
588/// `Eq ty a b`.
589#[allow(dead_code)]
590pub fn hm_eq(ty: HmExpr, a: HmExpr, b: HmExpr) -> HmExpr {
591    hm_app3(hm_cst("Eq"), ty, a, b)
592}
593/// `HashMap K V`.
594#[allow(dead_code)]
595pub fn hm_ty(k: HmExpr, v: HmExpr) -> HmExpr {
596    hm_app2(hm_cst("HashMap"), k, v)
597}
598/// `Option V`.
599#[allow(dead_code)]
600pub fn hm_option(v: HmExpr) -> HmExpr {
601    hm_app(hm_cst("Option"), v)
602}
603/// `Nat`.
604#[allow(dead_code)]
605pub fn hm_nat() -> HmExpr {
606    hm_cst("Nat")
607}
608/// `Bool`.
609#[allow(dead_code)]
610pub fn hm_bool() -> HmExpr {
611    hm_cst("Bool")
612}
613/// `List A`.
614#[allow(dead_code)]
615pub fn hm_list(a: HmExpr) -> HmExpr {
616    hm_app(hm_cst("List"), a)
617}
618/// `∀ {K V : Type}, HashMap K V → ...`  quantifier over a single map.
619#[allow(dead_code)]
620pub fn hm_ext_forall_map(body: HmExpr) -> HmExpr {
621    hm_pi(
622        HmBI::Implicit,
623        "K",
624        hm_type1(),
625        hm_pi(
626            HmBI::Implicit,
627            "V",
628            hm_type1(),
629            hm_pi(HmBI::Default, "m", hm_ty(hm_bvar(1), hm_bvar(0)), body),
630        ),
631    )
632}
633/// `∀ {K V : Type}, HashMap K V → HashMap K V → ...`
634#[allow(dead_code)]
635pub fn hm_ext_forall_two_maps(body: HmExpr) -> HmExpr {
636    hm_pi(
637        HmBI::Implicit,
638        "K",
639        hm_type1(),
640        hm_pi(
641            HmBI::Implicit,
642            "V",
643            hm_type1(),
644            hm_pi(
645                HmBI::Default,
646                "m1",
647                hm_ty(hm_bvar(1), hm_bvar(0)),
648                hm_pi(HmBI::Default, "m2", hm_ty(hm_bvar(2), hm_bvar(1)), body),
649            ),
650        ),
651    )
652}
653/// Equality of two `HashMap K V` values.
654#[allow(dead_code)]
655pub fn hm_ext_map_eq(k: HmExpr, v: HmExpr, a: HmExpr, b: HmExpr) -> HmExpr {
656    hm_eq(hm_ty(k, v), a, b)
657}
658/// Build `HashMap.get m k = Option.some v` equality.
659#[allow(dead_code)]
660pub fn hm_ext_get_eq_some(m: HmExpr, k: HmExpr, v: HmExpr, v_ty: HmExpr) -> HmExpr {
661    hm_eq(
662        hm_option(v_ty),
663        hm_app2(hm_cst("HashMap.get"), m, k),
664        hm_app(hm_cst("Option.some"), v),
665    )
666}
667/// Build `HashMap.get m k = Option.none`.
668#[allow(dead_code)]
669pub fn hm_ext_get_eq_none(m: HmExpr, k: HmExpr, v_ty: HmExpr) -> HmExpr {
670    hm_eq(
671        hm_option(v_ty),
672        hm_app2(hm_cst("HashMap.get"), m, k),
673        hm_cst("Option.none"),
674    )
675}
676/// Standard `∀ {K V} (m : HashMap K V) (k : K) (v : V)` prefix.
677#[allow(dead_code)]
678pub fn hm_ext_forall_map_k_v(body: HmExpr) -> HmExpr {
679    hm_pi(
680        HmBI::Implicit,
681        "K",
682        hm_type1(),
683        hm_pi(
684            HmBI::Implicit,
685            "V",
686            hm_type1(),
687            hm_pi(
688                HmBI::Default,
689                "m",
690                hm_ty(hm_bvar(1), hm_bvar(0)),
691                hm_pi(
692                    HmBI::Default,
693                    "k",
694                    hm_bvar(2),
695                    hm_pi(HmBI::Default, "v", hm_bvar(2), body),
696                ),
697            ),
698        ),
699    )
700}
oxilean_std/hashmap/functions.rs

oxilean_std/hashmap/
functions.rs
