oxilean_std/env_builder/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name, ReducibilityHint};
6
7use super::types::EnvBuilder;
8
9/// Build an `App` expression.
10pub fn app(f: Expr, a: Expr) -> Expr {
11    Expr::App(Box::new(f), Box::new(a))
12}
13/// Build an n-ary application from a function and argument list.
14pub fn app_n(f: Expr, args: Vec<Expr>) -> Expr {
15    args.into_iter().fold(f, app)
16}
17/// Build a `Const` expression (constant with no universe levels).
18pub fn var(name: &str) -> Expr {
19    Expr::Const(Name::str(name), vec![])
20}
21/// Build a bound variable expression at de Bruijn index `i`.
22pub fn bvar(i: u32) -> Expr {
23    Expr::BVar(i)
24}
25/// Build a `Sort(Level::zero())` (Prop).
26pub fn prop() -> Expr {
27    Expr::Sort(Level::zero())
28}
29/// Build a `Sort(Level::succ^n(Level::zero()))` (Type n-1).
30pub fn sort(n: u32) -> Expr {
31    let mut l = Level::zero();
32    for _ in 0..n {
33        l = Level::succ(l);
34    }
35    Expr::Sort(l)
36}
37/// Alias for `sort(1)` — `Type 0`.
38pub fn type0() -> Expr {
39    sort(1)
40}
41/// Alias for `sort(2)` — `Type 1`.
42pub fn type1() -> Expr {
43    sort(2)
44}
45/// Build a non-dependent arrow type `dom → cod`.
46pub fn pi(dom: Expr, cod: Expr) -> Expr {
47    Expr::Pi(
48        BinderInfo::Default,
49        Name::str("_"),
50        Box::new(dom),
51        Box::new(cod),
52    )
53}
54/// Build a named non-dependent pi-type `(name : dom) → cod`.
55pub fn pi_named(name: &str, dom: Expr, cod: Expr) -> Expr {
56    Expr::Pi(
57        BinderInfo::Default,
58        Name::str(name),
59        Box::new(dom),
60        Box::new(cod),
61    )
62}
63/// Build an implicit pi `{name : dom} → cod`.
64pub fn pi_implicit(name: &str, dom: Expr, cod: Expr) -> Expr {
65    Expr::Pi(
66        BinderInfo::Implicit,
67        Name::str(name),
68        Box::new(dom),
69        Box::new(cod),
70    )
71}
72/// Build an instance-implicit pi `[name : dom] → cod`.
73pub fn pi_inst(name: &str, dom: Expr, cod: Expr) -> Expr {
74    Expr::Pi(
75        BinderInfo::InstImplicit,
76        Name::str(name),
77        Box::new(dom),
78        Box::new(cod),
79    )
80}
81/// Build a `Lam` expression with an anonymous binder and `Prop` domain.
82pub fn lam(body: Expr) -> Expr {
83    Expr::Lam(
84        BinderInfo::Default,
85        Name::str("_"),
86        Box::new(prop()),
87        Box::new(body),
88    )
89}
90/// Build a named lambda `fun (name : ty) => body`.
91pub fn lam_named(name: &str, ty: Expr, body: Expr) -> Expr {
92    Expr::Lam(
93        BinderInfo::Default,
94        Name::str(name),
95        Box::new(ty),
96        Box::new(body),
97    )
98}
99/// Build an n-ary arrow type `t1 → t2 → … → ret`.
100pub fn arrows(mut tys: Vec<Expr>, ret: Expr) -> Expr {
101    tys.reverse();
102    tys.into_iter().fold(ret, |acc, t| pi(t, acc))
103}
104/// Add `Bool` with its constructors `Bool.true` and `Bool.false`.
105pub fn add_bool(b: &mut EnvBuilder) {
106    b.axiom("Bool", type0());
107    b.axiom("Bool.true", var("Bool"));
108    b.axiom("Bool.false", var("Bool"));
109}
110/// Add `Unit` with its constructor `Unit.unit`.
111pub fn add_unit(b: &mut EnvBuilder) {
112    b.axiom("Unit", type0());
113    b.axiom("Unit.unit", var("Unit"));
114}
115/// Add `Nat` with `Nat.zero` and `Nat.succ`.
116pub fn add_nat(b: &mut EnvBuilder) {
117    b.axiom("Nat", type0());
118    b.axiom("Nat.zero", var("Nat"));
119    b.axiom("Nat.succ", pi(var("Nat"), var("Nat")));
120}
121/// Add `Int` with `Int.ofNat` and `Int.negSucc`.
122pub fn add_int(b: &mut EnvBuilder) {
123    if !b.contains("Nat") {
124        add_nat(b);
125    }
126    b.axiom("Int", type0());
127    b.axiom("Int.ofNat", pi(var("Nat"), var("Int")));
128    b.axiom("Int.negSucc", pi(var("Nat"), var("Int")));
129}
130/// Add `Prod` (product type) with `Prod.mk`.
131pub fn add_prod(b: &mut EnvBuilder) {
132    b.axiom("Prod", pi(type0(), pi(type0(), type0())));
133    let prod_mk_ty = pi_implicit(
134        "α",
135        type0(),
136        pi_implicit(
137            "β",
138            type0(),
139            pi(
140                bvar(1),
141                pi(bvar(1), app(app(var("Prod"), bvar(3)), bvar(2))),
142            ),
143        ),
144    );
145    b.axiom("Prod.mk", prod_mk_ty);
146}
147/// Add `Option` with `Option.none` and `Option.some`.
148pub fn add_option(b: &mut EnvBuilder) {
149    b.axiom("Option", pi(type0(), type0()));
150    let none_ty = pi_implicit("α", type0(), app(var("Option"), bvar(0)));
151    b.axiom("Option.none", none_ty);
152    let some_ty = pi_implicit("α", type0(), pi(bvar(0), app(var("Option"), bvar(1))));
153    b.axiom("Option.some", some_ty);
154    // Option.map : {α β : Type} → (α → β) → Option α → Option β
155    let map_ty = pi_implicit(
156        "α",
157        type0(),
158        pi_implicit(
159            "β",
160            type0(),
161            pi(
162                pi(bvar(1), bvar(1)),
163                pi(app(var("Option"), bvar(2)), app(var("Option"), bvar(2))),
164            ),
165        ),
166    );
167    b.axiom("Option.map", map_ty);
168    // Option.bind : {α β : Type} → Option α → (α → Option β) → Option β
169    let bind_ty = pi_implicit(
170        "α",
171        type0(),
172        pi_implicit(
173            "β",
174            type0(),
175            pi(
176                app(var("Option"), bvar(1)),
177                pi(
178                    pi(bvar(2), app(var("Option"), bvar(2))),
179                    app(var("Option"), bvar(2)),
180                ),
181            ),
182        ),
183    );
184    b.axiom("Option.bind", bind_ty);
185    // Option.isSome : {α : Type} → Option α → Bool
186    let is_some_ty = pi_implicit("α", type0(), pi(app(var("Option"), bvar(0)), var("Bool")));
187    b.axiom("Option.isSome", is_some_ty);
188}
189/// Add `List` with `List.nil` and `List.cons`.
190pub fn add_list(b: &mut EnvBuilder) {
191    b.axiom("List", pi(type0(), type0()));
192    let nil_ty = pi_implicit("α", type0(), app(var("List"), bvar(0)));
193    b.axiom("List.nil", nil_ty);
194    let cons_ty = pi_implicit(
195        "α",
196        type0(),
197        pi(
198            bvar(0),
199            pi(app(var("List"), bvar(1)), app(var("List"), bvar(2))),
200        ),
201    );
202    b.axiom("List.cons", cons_ty);
203}
204/// Build a minimal standard prelude environment.
205pub fn minimal_prelude() -> Result<Environment, String> {
206    let mut b = EnvBuilder::fresh();
207    add_bool(&mut b);
208    add_unit(&mut b);
209    add_empty(&mut b);
210    add_nat(&mut b);
211    add_prod(&mut b);
212    add_option(&mut b);
213    add_list(&mut b);
214    b.finish()
215}
216#[cfg(test)]
217mod tests {
218    use super::*;
219    #[test]
220    fn test_builder_axiom() {
221        let mut b = EnvBuilder::fresh();
222        b.axiom("Foo", type0());
223        assert!(b.contains("Foo"));
224        assert!(b.is_ok());
225    }
226    #[test]
227    fn test_builder_def() {
228        let mut b = EnvBuilder::fresh();
229        b.axiom("Bool", type0());
230        b.def(
231            "myId",
232            pi(var("Bool"), var("Bool")),
233            lam_named("x", var("Bool"), bvar(0)),
234        );
235        assert!(b.is_ok());
236    }
237    #[test]
238    fn test_builder_finish_ok() {
239        let mut b = EnvBuilder::fresh();
240        b.axiom("Nat", type0());
241        let env = b.finish().expect("finish should succeed");
242        assert!(env.get(&Name::str("Nat")).is_some());
243    }
244    #[test]
245    fn test_add_bool() {
246        let mut b = EnvBuilder::fresh();
247        add_bool(&mut b);
248        assert!(b.contains("Bool"));
249        assert!(b.contains("Bool.true"));
250        assert!(b.contains("Bool.false"));
251    }
252    #[test]
253    fn test_add_nat() {
254        let mut b = EnvBuilder::fresh();
255        add_nat(&mut b);
256        assert!(b.contains("Nat"));
257        assert!(b.contains("Nat.zero"));
258        assert!(b.contains("Nat.succ"));
259    }
260    #[test]
261    fn test_add_list() {
262        let mut b = EnvBuilder::fresh();
263        add_list(&mut b);
264        assert!(b.contains("List"));
265        assert!(b.contains("List.nil"));
266        assert!(b.contains("List.cons"));
267    }
268    #[test]
269    fn test_add_option() {
270        let mut b = EnvBuilder::fresh();
271        add_option(&mut b);
272        assert!(b.contains("Option"));
273        assert!(b.contains("Option.none"));
274        assert!(b.contains("Option.some"));
275    }
276    #[test]
277    fn test_minimal_prelude() {
278        let env = minimal_prelude().expect("prelude should build");
279        for name in &[
280            "Bool", "Nat", "Int", "Unit", "Empty", "List", "Option", "Prod",
281        ] {
282            let _ = env.get(&Name::str(*name));
283        }
284        assert!(env.get(&Name::str("Bool")).is_some());
285        assert!(env.get(&Name::str("Nat")).is_some());
286    }
287    #[test]
288    fn test_app_n() {
289        let f = var("f");
290        let result = app_n(f, vec![bvar(0), bvar(1)]);
291        assert!(matches!(result, Expr::App(_, _)));
292    }
293    #[test]
294    fn test_arrows() {
295        let ty = arrows(vec![type0(), type0()], type0());
296        assert!(matches!(ty, Expr::Pi(_, _, _, _)));
297    }
298    #[test]
299    fn test_sort_levels() {
300        let p = prop();
301        let t = type0();
302        let t1 = type1();
303        assert!(matches!(p, Expr::Sort(_)));
304        assert!(matches!(t, Expr::Sort(_)));
305        assert!(matches!(t1, Expr::Sort(_)));
306    }
307    #[test]
308    fn test_builder_errors() {
309        let mut b = EnvBuilder::fresh();
310        b.axiom("X", type0());
311        b.axiom("X", type0());
312        assert!(!b.is_ok());
313        assert!(!b.errors().is_empty());
314    }
315    #[test]
316    fn test_add_int() {
317        let mut b = EnvBuilder::fresh();
318        add_nat(&mut b);
319        add_int(&mut b);
320        assert!(b.contains("Int"));
321        assert!(b.contains("Int.ofNat"));
322        assert!(b.contains("Int.negSucc"));
323    }
324}
325/// Add equality `Eq : {α : Type} → α → α → Prop`.
326#[allow(dead_code)]
327pub fn add_eq(b: &mut EnvBuilder) {
328    let eq_ty = pi_implicit("α", type0(), pi(bvar(0), pi(bvar(1), prop())));
329    b.axiom("Eq", eq_ty);
330    let refl_ty = pi_implicit(
331        "α",
332        type0(),
333        pi(bvar(0), app(app(app(var("Eq"), bvar(1)), bvar(0)), bvar(0))),
334    );
335    b.axiom("Eq.refl", refl_ty);
336}
337/// Add `And` (logical conjunction).
338#[allow(dead_code)]
339pub fn add_and(b: &mut EnvBuilder) {
340    b.axiom("And", pi(prop(), pi(prop(), prop())));
341    let intro_ty = pi(bvar(0), pi(bvar(1), app(app(var("And"), bvar(2)), bvar(1))));
342    b.axiom("And.intro", intro_ty);
343}
344/// Add `Or` (logical disjunction).
345#[allow(dead_code)]
346pub fn add_or(b: &mut EnvBuilder) {
347    b.axiom("Or", pi(prop(), pi(prop(), prop())));
348    let inl_ty = pi(bvar(0), app(app(var("Or"), bvar(1)), bvar(0)));
349    b.axiom("Or.inl", inl_ty);
350    let inr_ty = pi(bvar(0), app(app(var("Or"), bvar(0)), bvar(1)));
351    b.axiom("Or.inr", inr_ty);
352}
353/// Add `Not` (logical negation).
354#[allow(dead_code)]
355pub fn add_not(b: &mut EnvBuilder) {
356    b.axiom("Not", pi(prop(), prop()));
357}
358/// Add `False` (empty type in Prop).
359#[allow(dead_code)]
360pub fn add_false(b: &mut EnvBuilder) {
361    b.axiom("False", prop());
362    let elim_ty = pi_implicit("P", prop(), pi(var("False"), bvar(1)));
363    b.axiom("False.elim", elim_ty);
364}
365/// Add `True` (unit type in Prop).
366#[allow(dead_code)]
367pub fn add_true(b: &mut EnvBuilder) {
368    b.axiom("True", prop());
369    b.axiom("True.intro", var("True"));
370}
371/// Add `Iff` (logical biconditional).
372#[allow(dead_code)]
373pub fn add_iff(b: &mut EnvBuilder) {
374    b.axiom("Iff", pi(prop(), pi(prop(), prop())));
375    let intro_ty = pi(
376        pi(bvar(0), bvar(1)),
377        pi(pi(bvar(0), bvar(2)), app(app(var("Iff"), bvar(3)), bvar(2))),
378    );
379    b.axiom("Iff.intro", intro_ty);
380}
381/// Add `Exists` (existential quantifier).
382#[allow(dead_code)]
383pub fn add_exists(b: &mut EnvBuilder) {
384    let exists_ty = pi_implicit("α", type0(), pi(pi(bvar(0), prop()), prop()));
385    b.axiom("Exists", exists_ty);
386    let intro_ty = pi_implicit(
387        "α",
388        type0(),
389        pi_implicit(
390            "P",
391            pi(bvar(0), prop()),
392            pi(
393                bvar(1),
394                pi(app(bvar(1), bvar(0)), app(var("Exists"), bvar(2))),
395            ),
396        ),
397    );
398    b.axiom("Exists.intro", intro_ty);
399}
400/// Add `String` type.
401#[allow(dead_code)]
402pub fn add_string(b: &mut EnvBuilder) {
403    b.axiom("String", type0());
404}
405/// Add `Char` type.
406#[allow(dead_code)]
407pub fn add_char(b: &mut EnvBuilder) {
408    b.axiom("Char", type0());
409}
410/// Build a full logic prelude (Bool, Nat, Eq, And, Or, Not, True, False, Iff, Exists).
411#[allow(dead_code)]
412pub fn logic_prelude() -> Result<Environment, String> {
413    let mut b = EnvBuilder::fresh();
414    add_bool(&mut b);
415    add_nat(&mut b);
416    add_true(&mut b);
417    add_false(&mut b);
418    add_not(&mut b);
419    add_and(&mut b);
420    add_or(&mut b);
421    add_iff(&mut b);
422    add_eq(&mut b);
423    add_exists(&mut b);
424    b.finish()
425}
426/// Build the type of an identity function `{α : Type} → α → α`.
427#[allow(dead_code)]
428pub fn id_type() -> Expr {
429    pi_implicit("α", type0(), pi(bvar(0), bvar(1)))
430}
431/// Build the type of a composition function
432/// `{α β γ : Type} → (β → γ) → (α → β) → α → γ`.
433#[allow(dead_code)]
434pub fn compose_type() -> Expr {
435    pi_implicit(
436        "α",
437        type0(),
438        pi_implicit(
439            "β",
440            type0(),
441            pi_implicit(
442                "γ",
443                type0(),
444                pi(
445                    pi(bvar(1), bvar(2)),
446                    pi(pi(bvar(2), bvar(2)), pi(bvar(3), bvar(2))),
447                ),
448            ),
449        ),
450    )
451}
452#[cfg(test)]
453mod env_builder_extra_tests {
454    use super::*;
455    #[test]
456    fn test_add_eq() {
457        let mut b = EnvBuilder::fresh();
458        add_eq(&mut b);
459        assert!(b.contains("Eq"));
460        assert!(b.contains("Eq.refl"));
461    }
462    #[test]
463    fn test_add_and_or() {
464        let mut b = EnvBuilder::fresh();
465        add_and(&mut b);
466        add_or(&mut b);
467        assert!(b.contains("And"));
468        assert!(b.contains("Or"));
469        assert!(b.contains("Or.inl"));
470        assert!(b.contains("Or.inr"));
471    }
472    #[test]
473    fn test_add_not_false_true() {
474        let mut b = EnvBuilder::fresh();
475        add_not(&mut b);
476        add_false(&mut b);
477        add_true(&mut b);
478        assert!(b.contains("Not"));
479        assert!(b.contains("False"));
480        assert!(b.contains("True"));
481        assert!(b.contains("True.intro"));
482        assert!(b.contains("False.elim"));
483    }
484    #[test]
485    fn test_add_iff() {
486        let mut b = EnvBuilder::fresh();
487        add_iff(&mut b);
488        assert!(b.contains("Iff"));
489        assert!(b.contains("Iff.intro"));
490    }
491    #[test]
492    fn test_add_exists() {
493        let mut b = EnvBuilder::fresh();
494        add_exists(&mut b);
495        assert!(b.contains("Exists"));
496        assert!(b.contains("Exists.intro"));
497    }
498    #[test]
499    fn test_logic_prelude() {
500        let env = logic_prelude().expect("logic prelude should build");
501        for name in &["Bool", "Nat", "And", "Or", "Not", "Iff", "Eq", "Exists"] {
502            assert!(env.get(&Name::str(*name)).is_some(), "missing {}", name);
503        }
504    }
505    #[test]
506    fn test_id_type() {
507        let ty = id_type();
508        assert!(matches!(ty, Expr::Pi(_, _, _, _)));
509    }
510    #[test]
511    fn test_builder_theorem() {
512        let mut b = EnvBuilder::fresh();
513        add_true(&mut b);
514        b.theorem("my_thm", var("True"), var("True.intro"));
515        assert!(b.is_ok());
516    }
517    #[test]
518    fn test_add_string_char() {
519        let mut b = EnvBuilder::fresh();
520        add_string(&mut b);
521        add_char(&mut b);
522        assert!(b.contains("String"));
523        assert!(b.contains("Char"));
524    }
525    #[test]
526    fn test_pi_variants() {
527        let p = pi_named("x", type0(), type0());
528        assert!(matches!(p, Expr::Pi(BinderInfo::Default, _, _, _)));
529        let imp = pi_implicit("y", type0(), type0());
530        assert!(matches!(imp, Expr::Pi(BinderInfo::Implicit, _, _, _)));
531        let inst = pi_inst("z", type0(), type0());
532        assert!(matches!(inst, Expr::Pi(BinderInfo::InstImplicit, _, _, _)));
533    }
534}
535/// Add `WellFounded` typeclass stub.
536#[allow(dead_code)]
537pub fn add_well_founded(b: &mut EnvBuilder) {
538    let wf_ty = pi_implicit("α", type0(), pi(pi(bvar(0), pi(bvar(1), prop())), prop()));
539    b.axiom("WellFounded", wf_ty);
540    // WellFounded.rec : {α : Type} → {r : α → α → Prop} → {C : α → Type}
541    //   → ((x : α) → ((y : α) → r y x → C y) → C x) → (w : WellFounded r) → (a : α) → C a
542    // Simplified: {α : Type} → {r : α → α → Prop} → WellFounded r → α → Type
543    let rec_ty = pi_implicit(
544        "α",
545        type0(),
546        pi_implicit(
547            "r",
548            pi(bvar(0), pi(bvar(1), prop())),
549            pi(prop(), pi(bvar(2), type0())),
550        ),
551    );
552    b.axiom("WellFounded.rec", rec_ty);
553    // Acc : {α : Type} → (α → α → Prop) → α → Prop
554    let acc_ty = pi_implicit(
555        "α",
556        type0(),
557        pi(pi(bvar(0), pi(bvar(1), prop())), pi(bvar(1), prop())),
558    );
559    b.axiom("Acc", acc_ty);
560    // Acc.intro : {α : Type} → {r : α → α → Prop} → (x : α) → ((y : α) → r y x → Acc r y) → Acc r x
561    // Simplified: {α : Type} → {r : α → α → Prop} → α → Prop
562    let acc_intro_ty = pi_implicit(
563        "α",
564        type0(),
565        pi_implicit("r", pi(bvar(0), pi(bvar(1), prop())), pi(bvar(1), prop())),
566    );
567    b.axiom("Acc.intro", acc_intro_ty);
568}
569/// Add `Decidable` typeclass stub.
570#[allow(dead_code)]
571pub fn add_decidable(b: &mut EnvBuilder) {
572    b.axiom("Decidable", pi(prop(), type0()));
573    let is_true_ty = pi_implicit("P", prop(), pi(bvar(0), app(var("Decidable"), bvar(1))));
574    b.axiom("Decidable.isTrue", is_true_ty);
575    let is_false_ty = pi_implicit(
576        "P",
577        prop(),
578        pi(pi(bvar(0), var("False")), app(var("Decidable"), bvar(1))),
579    );
580    b.axiom("Decidable.isFalse", is_false_ty);
581    // decide : {P : Prop} → [Decidable P] → Decidable P
582    let decide_ty = pi_implicit("P", prop(), app(var("Decidable"), bvar(0)));
583    b.axiom("decide", decide_ty);
584    // instDecidableAnd : {P Q : Prop} → [Decidable P] → [Decidable Q] → Decidable (P ∧ Q)
585    let and_ty = pi_implicit(
586        "P",
587        prop(),
588        pi_implicit(
589            "Q",
590            prop(),
591            pi(
592                app(var("Decidable"), bvar(1)),
593                pi(
594                    app(var("Decidable"), bvar(1)),
595                    app(var("Decidable"), app(app(var("And"), bvar(3)), bvar(2))),
596                ),
597            ),
598        ),
599    );
600    b.axiom("instDecidableAnd", and_ty);
601}
602/// Add `Subtype` type.
603#[allow(dead_code)]
604pub fn add_subtype(b: &mut EnvBuilder) {
605    let subtype_ty = pi_implicit("α", type0(), pi(pi(bvar(0), prop()), type0()));
606    b.axiom("Subtype", subtype_ty);
607    let mk_ty = pi_implicit(
608        "α",
609        type0(),
610        pi_implicit(
611            "P",
612            pi(bvar(0), prop()),
613            pi(
614                bvar(1),
615                pi(app(bvar(1), bvar(0)), app(var("Subtype"), bvar(2))),
616            ),
617        ),
618    );
619    b.axiom("Subtype.mk", mk_ty);
620    // Subtype.val : {α : Type} → {P : α → Prop} → Subtype P → α
621    let val_ty = pi_implicit(
622        "α",
623        type0(),
624        pi_implicit(
625            "P",
626            pi(bvar(0), prop()),
627            pi(app(var("Subtype"), bvar(0)), bvar(2)),
628        ),
629    );
630    b.axiom("Subtype.val", val_ty);
631    // Subtype.property : {α : Type} → {P : α → Prop} → (s : Subtype P) → P (Subtype.val s)
632    // Simplified: Subtype P → Prop
633    let prop_ty = pi_implicit(
634        "α",
635        type0(),
636        pi_implicit(
637            "P",
638            pi(bvar(0), prop()),
639            pi(app(var("Subtype"), bvar(0)), prop()),
640        ),
641    );
642    b.axiom("Subtype.property", prop_ty);
643}
644#[cfg(test)]
645mod env_builder_final_tests {
646    use super::*;
647    #[test]
648    fn test_add_well_founded() {
649        let mut b = EnvBuilder::fresh();
650        add_well_founded(&mut b);
651        assert!(b.contains("WellFounded"));
652    }
653    #[test]
654    fn test_add_decidable() {
655        let mut b = EnvBuilder::fresh();
656        add_false(&mut b);
657        add_decidable(&mut b);
658        assert!(b.contains("Decidable"));
659        assert!(b.contains("Decidable.isTrue"));
660        assert!(b.contains("Decidable.isFalse"));
661    }
662    #[test]
663    fn test_add_subtype() {
664        let mut b = EnvBuilder::fresh();
665        add_subtype(&mut b);
666        assert!(b.contains("Subtype"));
667        assert!(b.contains("Subtype.mk"));
668    }
669}
670/// Add `Functor` typeclass stub.
671#[allow(dead_code)]
672pub fn add_functor(b: &mut EnvBuilder) {
673    b.axiom("Functor", pi(pi(type0(), type0()), type1()));
674    let map_ty = pi_implicit(
675        "F",
676        pi(type0(), type0()),
677        pi_inst(
678            "_",
679            app(var("Functor"), bvar(0)),
680            pi_implicit(
681                "α",
682                type0(),
683                pi_implicit(
684                    "β",
685                    type0(),
686                    pi(
687                        pi(bvar(1), bvar(1)),
688                        pi(app(bvar(4), bvar(2)), app(bvar(5), bvar(2))),
689                    ),
690                ),
691            ),
692        ),
693    );
694    b.axiom("Functor.map", map_ty);
695}
696/// Add `Monad` typeclass stub.
697#[allow(dead_code)]
698pub fn add_monad(b: &mut EnvBuilder) {
699    b.axiom("Monad", pi(pi(type0(), type0()), type1()));
700    let pure_ty = pi_implicit(
701        "M",
702        pi(type0(), type0()),
703        pi_inst(
704            "_",
705            app(var("Monad"), bvar(0)),
706            pi_implicit("α", type0(), pi(bvar(0), app(bvar(3), bvar(1)))),
707        ),
708    );
709    b.axiom("Monad.pure", pure_ty);
710}
711#[cfg(test)]
712mod env_builder_monad_tests {
713    use super::*;
714    #[test]
715    fn test_add_functor() {
716        let mut b = EnvBuilder::fresh();
717        add_functor(&mut b);
718        assert!(b.contains("Functor"));
719        assert!(b.contains("Functor.map"));
720    }
721    #[test]
722    fn test_add_monad() {
723        let mut b = EnvBuilder::fresh();
724        add_monad(&mut b);
725        assert!(b.contains("Monad"));
726        assert!(b.contains("Monad.pure"));
727    }
728}
729/// Add `Sigma` (dependent pair) type.
730#[allow(dead_code)]
731pub fn add_sigma(b: &mut EnvBuilder) {
732    let sigma_ty = pi_implicit("α", type0(), pi(pi(bvar(0), type0()), type0()));
733    b.axiom("Sigma", sigma_ty);
734    let mk_ty = pi_implicit(
735        "α",
736        type0(),
737        pi_implicit(
738            "β",
739            pi(bvar(0), type0()),
740            pi(
741                bvar(1),
742                pi(app(bvar(1), bvar(0)), app(var("Sigma"), bvar(2))),
743            ),
744        ),
745    );
746    b.axiom("Sigma.mk", mk_ty);
747    let fst_ty = pi_implicit(
748        "α",
749        type0(),
750        pi_implicit(
751            "β",
752            pi(bvar(0), type0()),
753            pi(app(var("Sigma"), bvar(0)), bvar(2)),
754        ),
755    );
756    b.axiom("Sigma.fst", fst_ty);
757    // Sigma.snd : {α : Type} → {β : α → Type} → (s : Sigma β) → β (Sigma.fst s)
758    // Simplified type: Sigma β → Type (approximate)
759    let snd_ty = pi_implicit(
760        "α",
761        type0(),
762        pi_implicit(
763            "β",
764            pi(bvar(0), type0()),
765            pi(app(var("Sigma"), bvar(0)), type0()),
766        ),
767    );
768    b.axiom("Sigma.snd", snd_ty);
769}
770/// Add `Empty` (the uninhabited type).
771#[allow(dead_code)]
772pub fn add_empty(b: &mut EnvBuilder) {
773    b.axiom("Empty", type0());
774    let elim_ty = pi_implicit("α", type0(), pi(var("Empty"), bvar(1)));
775    b.axiom("Empty.elim", elim_ty);
776}
777/// Add `Unit` type with constructor.
778#[allow(dead_code)]
779pub fn add_unit_full(b: &mut EnvBuilder) {
780    b.axiom("Unit", type0());
781    b.axiom("Unit.star", var("Unit"));
782    let rec_ty = pi_implicit("α", type0(), pi(bvar(0), pi(var("Unit"), bvar(2))));
783    b.axiom("Unit.rec", rec_ty);
784}
785/// Add `Fin n` (finite type with n elements).
786#[allow(dead_code)]
787pub fn add_fin(b: &mut EnvBuilder) {
788    b.axiom("Fin", pi(var("Nat"), type0()));
789    let mk_ty = pi(var("Nat"), pi(var("Nat"), app(var("Fin"), bvar(1))));
790    b.axiom("Fin.mk", mk_ty);
791    let val_ty = pi_implicit("n", var("Nat"), pi(app(var("Fin"), bvar(0)), var("Nat")));
792    b.axiom("Fin.val", val_ty);
793    // Fin.zero : {n : Nat} → Fin (n + 1)
794    let zero_ty = pi_implicit(
795        "n",
796        var("Nat"),
797        app(
798            var("Fin"),
799            app(
800                app(var("Nat.add"), bvar(0)),
801                app(var("Nat.succ"), var("Nat.zero")),
802            ),
803        ),
804    );
805    b.axiom("Fin.zero", zero_ty);
806}
807/// Add `Array α` type (dynamic array).
808#[allow(dead_code)]
809pub fn add_array(b: &mut EnvBuilder) {
810    b.axiom("Array", pi(type0(), type0()));
811    let empty_ty = pi_implicit("α", type0(), app(var("Array"), bvar(0)));
812    b.axiom("Array.empty", empty_ty);
813    let push_ty = pi_implicit(
814        "α",
815        type0(),
816        pi(
817            app(var("Array"), bvar(0)),
818            pi(bvar(1), app(var("Array"), bvar(2))),
819        ),
820    );
821    b.axiom("Array.push", push_ty);
822    let size_ty = pi_implicit("α", type0(), pi(app(var("Array"), bvar(0)), var("Nat")));
823    b.axiom("Array.size", size_ty);
824}
825/// Add `HashMap K V` type.
826#[allow(dead_code)]
827pub fn add_hashmap(b: &mut EnvBuilder) {
828    b.axiom("HashMap", pi(type0(), pi(type0(), type0())));
829    let empty_ty = pi_implicit(
830        "K",
831        type0(),
832        pi_implicit("V", type0(), app(app(var("HashMap"), bvar(1)), bvar(0))),
833    );
834    b.axiom("HashMap.empty", empty_ty);
835    let insert_ty = pi_implicit(
836        "K",
837        type0(),
838        pi_implicit(
839            "V",
840            type0(),
841            pi(
842                app(app(var("HashMap"), bvar(1)), bvar(0)),
843                pi(
844                    bvar(2),
845                    pi(bvar(2), app(app(var("HashMap"), bvar(4)), bvar(3))),
846                ),
847            ),
848        ),
849    );
850    b.axiom("HashMap.insert", insert_ty);
851}
852/// Add `IO α` effect type.
853#[allow(dead_code)]
854pub fn add_io(b: &mut EnvBuilder) {
855    b.axiom("IO", pi(type0(), type0()));
856    let pure_ty = pi_implicit("α", type0(), pi(bvar(0), app(var("IO"), bvar(1))));
857    b.axiom("IO.pure", pure_ty);
858    let bind_ty = pi_implicit(
859        "α",
860        type0(),
861        pi_implicit(
862            "β",
863            type0(),
864            pi(
865                app(var("IO"), bvar(1)),
866                pi(
867                    pi(bvar(2), app(var("IO"), bvar(2))),
868                    app(var("IO"), bvar(2)),
869                ),
870            ),
871        ),
872    );
873    b.axiom("IO.bind", bind_ty);
874}
875#[cfg(test)]
876mod env_builder_extended_tests {
877    use super::*;
878    #[test]
879    fn test_add_sigma() {
880        let mut b = EnvBuilder::fresh();
881        add_sigma(&mut b);
882        assert!(b.contains("Sigma"));
883        assert!(b.contains("Sigma.mk"));
884        assert!(b.contains("Sigma.fst"));
885    }
886    #[test]
887    fn test_add_empty() {
888        let mut b = EnvBuilder::fresh();
889        add_empty(&mut b);
890        assert!(b.contains("Empty"));
891        assert!(b.contains("Empty.elim"));
892    }
893    #[test]
894    fn test_add_unit_full() {
895        let mut b = EnvBuilder::fresh();
896        add_unit_full(&mut b);
897        assert!(b.contains("Unit"));
898        assert!(b.contains("Unit.star"));
899        assert!(b.contains("Unit.rec"));
900    }
901    #[test]
902    fn test_add_fin() {
903        let mut b = EnvBuilder::fresh();
904        b.axiom("Nat", type0());
905        add_fin(&mut b);
906        assert!(b.contains("Fin"));
907        assert!(b.contains("Fin.mk"));
908        assert!(b.contains("Fin.val"));
909    }
910    #[test]
911    fn test_add_array() {
912        let mut b = EnvBuilder::fresh();
913        b.axiom("Nat", type0());
914        add_array(&mut b);
915        assert!(b.contains("Array"));
916        assert!(b.contains("Array.empty"));
917        assert!(b.contains("Array.push"));
918        assert!(b.contains("Array.size"));
919    }
920    #[test]
921    fn test_add_hashmap() {
922        let mut b = EnvBuilder::fresh();
923        add_hashmap(&mut b);
924        assert!(b.contains("HashMap"));
925        assert!(b.contains("HashMap.empty"));
926        assert!(b.contains("HashMap.insert"));
927    }
928    #[test]
929    fn test_add_io() {
930        let mut b = EnvBuilder::fresh();
931        add_io(&mut b);
932        assert!(b.contains("IO"));
933        assert!(b.contains("IO.pure"));
934        assert!(b.contains("IO.bind"));
935    }
936    #[test]
937    fn test_builder_is_ok_after_additions() {
938        let mut b = EnvBuilder::fresh();
939        add_empty(&mut b);
940        add_unit_full(&mut b);
941        assert!(b.is_ok());
942    }
943}
944/// Build a lambda abstraction `fun (name : dom) => body` (extended version).
945#[allow(dead_code)]
946pub fn lam_ext(name: &str, dom: Expr, body: Expr) -> Expr {
947    Expr::Lam(
948        BinderInfo::Default,
949        Name::str(name),
950        Box::new(dom),
951        Box::new(body),
952    )
953}
954/// Build `Sort(Level::Param("u"))` — a polymorphic sort.
955#[allow(dead_code)]
956pub fn sort_u() -> Expr {
957    Expr::Sort(Level::Param(Name::str("u")))
958}
959/// Build `Sort(Level::Param("v"))`.
960#[allow(dead_code)]
961pub fn sort_v() -> Expr {
962    Expr::Sort(Level::Param(Name::str("v")))
963}
964/// Build a chain of non-dependent pi-types: A₁ → A₂ → … → ret.
965#[allow(dead_code)]
966pub fn pi_chain(domains: Vec<Expr>, ret: Expr) -> Expr {
967    domains.into_iter().rev().fold(ret, |acc, dom| pi(dom, acc))
968}
969/// Build a `Const` with one universe parameter `u`.
970#[allow(dead_code)]
971pub fn var_u(name: &str) -> Expr {
972    Expr::Const(Name::str(name), vec![Level::Param(Name::str("u"))])
973}
974/// Add propositional logic connectives (True, False, And, Or, Not, Iff, And.intro, etc.)
975#[allow(dead_code)]
976pub fn add_prop_logic(b: &mut EnvBuilder) {
977    b.axiom("True", prop());
978    b.axiom("False", prop());
979    b.axiom("And", pi(prop(), pi(prop(), prop())));
980    b.axiom("Or", pi(prop(), pi(prop(), prop())));
981    b.axiom("Not", pi(prop(), prop()));
982    b.axiom("Iff", pi(prop(), pi(prop(), prop())));
983    b.axiom(
984        "And.intro",
985        pi_named(
986            "p",
987            prop(),
988            pi_named(
989                "q",
990                prop(),
991                pi(bvar(1), pi(bvar(1), app(app(var("And"), bvar(3)), bvar(2)))),
992            ),
993        ),
994    );
995    b.axiom(
996        "And.left",
997        pi_named(
998            "p",
999            prop(),
1000            pi_named(
1001                "q",
1002                prop(),
1003                pi(app(app(var("And"), bvar(1)), bvar(0)), bvar(2)),
1004            ),
1005        ),
1006    );
1007    b.axiom(
1008        "And.right",
1009        pi_named(
1010            "p",
1011            prop(),
1012            pi_named(
1013                "q",
1014                prop(),
1015                pi(app(app(var("And"), bvar(1)), bvar(0)), bvar(1)),
1016            ),
1017        ),
1018    );
1019    b.axiom(
1020        "Or.inl",
1021        pi_named(
1022            "p",
1023            prop(),
1024            pi_named(
1025                "q",
1026                prop(),
1027                pi(bvar(1), app(app(var("Or"), bvar(2)), bvar(1))),
1028            ),
1029        ),
1030    );
1031    b.axiom(
1032        "Or.inr",
1033        pi_named(
1034            "p",
1035            prop(),
1036            pi_named(
1037                "q",
1038                prop(),
1039                pi(bvar(0), app(app(var("Or"), bvar(2)), bvar(1))),
1040            ),
1041        ),
1042    );
1043}
1044/// Add extended `Nat` arithmetic: add, mul, sub, div, mod, pow, gcd, lcm, factorial.
1045#[allow(dead_code)]
1046pub fn add_nat_arith(b: &mut EnvBuilder) {
1047    if !b.contains("Nat") {
1048        b.axiom("Nat", type0());
1049        b.axiom("Nat.zero", var("Nat"));
1050        b.axiom("Nat.succ", pi(var("Nat"), var("Nat")));
1051    }
1052    b.axiom("Nat.add", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1053    b.axiom("Nat.mul", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1054    b.axiom("Nat.sub", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1055    b.axiom("Nat.div", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1056    b.axiom("Nat.mod", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1057    b.axiom("Nat.pow", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1058    b.axiom("Nat.gcd", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1059    b.axiom("Nat.lcm", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1060    b.axiom("Nat.factorial", pi(var("Nat"), var("Nat")));
1061    b.axiom("Nat.lt", pi(var("Nat"), pi(var("Nat"), prop())));
1062    b.axiom("Nat.le", pi(var("Nat"), pi(var("Nat"), prop())));
1063    b.axiom("Nat.min", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1064    b.axiom("Nat.max", pi(var("Nat"), pi(var("Nat"), var("Nat"))));
1065    b.axiom("Nat.toInt", pi(var("Nat"), var("Int")));
1066    b.axiom("Nat.repr", pi(var("Nat"), var("String")));
1067}
1068/// Add `Int` arithmetic operations.
1069#[allow(dead_code)]
1070pub fn add_int_arith(b: &mut EnvBuilder) {
1071    if !b.contains("Int") {
1072        b.axiom("Int", type0());
1073    }
1074    b.axiom("Int.add", pi(var("Int"), pi(var("Int"), var("Int"))));
1075    b.axiom("Int.sub", pi(var("Int"), pi(var("Int"), var("Int"))));
1076    b.axiom("Int.mul", pi(var("Int"), pi(var("Int"), var("Int"))));
1077    b.axiom("Int.div", pi(var("Int"), pi(var("Int"), var("Int"))));
1078    b.axiom("Int.mod", pi(var("Int"), pi(var("Int"), var("Int"))));
1079    b.axiom("Int.neg", pi(var("Int"), var("Int")));
1080    b.axiom("Int.abs", pi(var("Int"), var("Nat")));
1081    b.axiom("Int.lt", pi(var("Int"), pi(var("Int"), prop())));
1082    b.axiom("Int.le", pi(var("Int"), pi(var("Int"), prop())));
1083    b.axiom("Int.gcd", pi(var("Int"), pi(var("Int"), var("Nat"))));
1084}
1085/// Add `Float` operations.
1086#[allow(dead_code)]
1087pub fn add_float_ops(b: &mut EnvBuilder) {
1088    b.axiom("Float", type0());
1089    b.axiom(
1090        "Float.add",
1091        pi(var("Float"), pi(var("Float"), var("Float"))),
1092    );
1093    b.axiom(
1094        "Float.sub",
1095        pi(var("Float"), pi(var("Float"), var("Float"))),
1096    );
1097    b.axiom(
1098        "Float.mul",
1099        pi(var("Float"), pi(var("Float"), var("Float"))),
1100    );
1101    b.axiom(
1102        "Float.div",
1103        pi(var("Float"), pi(var("Float"), var("Float"))),
1104    );
1105    b.axiom("Float.neg", pi(var("Float"), var("Float")));
1106    b.axiom("Float.abs", pi(var("Float"), var("Float")));
1107    b.axiom("Float.sqrt", pi(var("Float"), var("Float")));
1108    b.axiom("Float.exp", pi(var("Float"), var("Float")));
1109    b.axiom("Float.log", pi(var("Float"), var("Float")));
1110    b.axiom("Float.sin", pi(var("Float"), var("Float")));
1111    b.axiom("Float.cos", pi(var("Float"), var("Float")));
1112    b.axiom("Float.tan", pi(var("Float"), var("Float")));
1113    b.axiom(
1114        "Float.pow",
1115        pi(var("Float"), pi(var("Float"), var("Float"))),
1116    );
1117    b.axiom("Float.floor", pi(var("Float"), var("Float")));
1118    b.axiom("Float.ceil", pi(var("Float"), var("Float")));
1119    b.axiom("Float.round", pi(var("Float"), var("Float")));
1120    b.axiom("Float.lt", pi(var("Float"), pi(var("Float"), prop())));
1121    b.axiom("Float.le", pi(var("Float"), pi(var("Float"), prop())));
1122    b.axiom("Float.isNaN", pi(var("Float"), var("Bool")));
1123    b.axiom("Float.isInf", pi(var("Float"), var("Bool")));
1124    b.axiom("Float.ofNat", pi(var("Nat"), var("Float")));
1125}
1126/// Add `String` operations.
1127#[allow(dead_code)]
1128pub fn add_string_ops(b: &mut EnvBuilder) {
1129    if !b.contains("String") {
1130        b.axiom("String", type0());
1131    }
1132    b.axiom("String.empty", var("String"));
1133    b.axiom(
1134        "String.append",
1135        pi(var("String"), pi(var("String"), var("String"))),
1136    );
1137    b.axiom("String.length", pi(var("String"), var("Nat")));
1138    b.axiom("String.get", pi(var("String"), pi(var("Nat"), var("Char"))));
1139    b.axiom("String.toLower", pi(var("String"), var("String")));
1140    b.axiom("String.toUpper", pi(var("String"), var("String")));
1141    b.axiom("String.trim", pi(var("String"), var("String")));
1142    b.axiom(
1143        "String.beq",
1144        pi(var("String"), pi(var("String"), var("Bool"))),
1145    );
1146    b.axiom("String.lt", pi(var("String"), pi(var("String"), prop())));
1147    b.axiom("String.repr", pi(var("String"), var("String")));
1148}
1149/// Add `Char` operations.
1150#[allow(dead_code)]
1151pub fn add_char_ops(b: &mut EnvBuilder) {
1152    if !b.contains("Char") {
1153        b.axiom("Char", type0());
1154    }
1155    b.axiom("Char.val", pi(var("Char"), var("Nat")));
1156    b.axiom("Char.ofNat", pi(var("Nat"), var("Char")));
1157    b.axiom("Char.isAlpha", pi(var("Char"), var("Bool")));
1158    b.axiom("Char.isDigit", pi(var("Char"), var("Bool")));
1159    b.axiom("Char.isSpace", pi(var("Char"), var("Bool")));
1160    b.axiom("Char.isUpper", pi(var("Char"), var("Bool")));
1161    b.axiom("Char.isLower", pi(var("Char"), var("Bool")));
1162    b.axiom("Char.toUpper", pi(var("Char"), var("Char")));
1163    b.axiom("Char.toLower", pi(var("Char"), var("Char")));
1164    b.axiom("Char.beq", pi(var("Char"), pi(var("Char"), var("Bool"))));
1165}
1166/// Add `Result` type with `.ok`, `.err`, `.isOk`, `.isErr`.
1167#[allow(dead_code)]
1168pub fn add_result(b: &mut EnvBuilder) {
1169    b.axiom("Result", pi(type0(), pi(type0(), type0())));
1170    b.axiom(
1171        "Result.ok",
1172        pi_implicit(
1173            "α",
1174            type0(),
1175            pi_implicit(
1176                "ε",
1177                type0(),
1178                pi(bvar(1), app(app(var("Result"), bvar(2)), bvar(1))),
1179            ),
1180        ),
1181    );
1182    b.axiom(
1183        "Result.err",
1184        pi_implicit(
1185            "α",
1186            type0(),
1187            pi_implicit(
1188                "ε",
1189                type0(),
1190                pi(bvar(0), app(app(var("Result"), bvar(2)), bvar(1))),
1191            ),
1192        ),
1193    );
1194    b.axiom(
1195        "Result.isOk",
1196        pi_implicit(
1197            "α",
1198            type0(),
1199            pi_implicit(
1200                "ε",
1201                type0(),
1202                pi(app(app(var("Result"), bvar(1)), bvar(0)), var("Bool")),
1203            ),
1204        ),
1205    );
1206    b.axiom(
1207        "Result.isErr",
1208        pi_implicit(
1209            "α",
1210            type0(),
1211            pi_implicit(
1212                "ε",
1213                type0(),
1214                pi(app(app(var("Result"), bvar(1)), bvar(0)), var("Bool")),
1215            ),
1216        ),
1217    );
1218}
1219/// Add `StateT` monad transformer.
1220#[allow(dead_code)]
1221pub fn add_state_monad(b: &mut EnvBuilder) {
1222    b.axiom("StateT", pi(type0(), pi(type0(), pi(type0(), type0()))));
1223    b.axiom(
1224        "StateT.pure",
1225        pi_implicit(
1226            "σ",
1227            type0(),
1228            pi_implicit(
1229                "m",
1230                type0(),
1231                pi_implicit(
1232                    "α",
1233                    type0(),
1234                    pi(
1235                        bvar(0),
1236                        app(app(app(var("StateT"), bvar(3)), bvar(2)), bvar(1)),
1237                    ),
1238                ),
1239            ),
1240        ),
1241    );
1242    b.axiom(
1243        "StateT.bind",
1244        pi_implicit(
1245            "σ",
1246            type0(),
1247            pi_implicit(
1248                "m",
1249                type0(),
1250                pi_implicit(
1251                    "α",
1252                    type0(),
1253                    pi_implicit(
1254                        "β",
1255                        type0(),
1256                        pi(
1257                            app(app(app(var("StateT"), bvar(3)), bvar(2)), bvar(1)),
1258                            pi(
1259                                pi(
1260                                    bvar(2),
1261                                    app(app(app(var("StateT"), bvar(4)), bvar(3)), bvar(1)),
1262                                ),
1263                                app(app(app(var("StateT"), bvar(4)), bvar(3)), bvar(1)),
1264                            ),
1265                        ),
1266                    ),
1267                ),
1268            ),
1269        ),
1270    );
1271    b.axiom(
1272        "StateT.get",
1273        pi_implicit(
1274            "σ",
1275            type0(),
1276            pi_implicit(
1277                "m",
1278                type0(),
1279                app(app(app(var("StateT"), bvar(1)), bvar(0)), bvar(1)),
1280            ),
1281        ),
1282    );
1283    b.axiom(
1284        "StateT.set",
1285        pi_implicit(
1286            "σ",
1287            type0(),
1288            pi_implicit(
1289                "m",
1290                type0(),
1291                pi(
1292                    bvar(1),
1293                    app(app(app(var("StateT"), bvar(2)), bvar(1)), var("Unit")),
1294                ),
1295            ),
1296        ),
1297    );
1298    b.axiom(
1299        "StateT.modify",
1300        pi_implicit(
1301            "σ",
1302            type0(),
1303            pi_implicit(
1304                "m",
1305                type0(),
1306                pi(
1307                    pi(bvar(1), bvar(2)),
1308                    app(app(app(var("StateT"), bvar(2)), bvar(1)), var("Unit")),
1309                ),
1310            ),
1311        ),
1312    );
1313    b.axiom(
1314        "StateT.run",
1315        pi_implicit(
1316            "σ",
1317            type0(),
1318            pi_implicit(
1319                "m",
1320                type0(),
1321                pi_implicit(
1322                    "α",
1323                    type0(),
1324                    pi(
1325                        app(app(app(var("StateT"), bvar(2)), bvar(1)), bvar(0)),
1326                        pi(bvar(3), bvar(3)),
1327                    ),
1328                ),
1329            ),
1330        ),
1331    );
1332}
1333/// Add `ReaderT` monad transformer.
1334#[allow(dead_code)]
1335pub fn add_reader_monad(b: &mut EnvBuilder) {
1336    b.axiom("ReaderT", pi(type0(), pi(type0(), pi(type0(), type0()))));
1337    b.axiom(
1338        "ReaderT.pure",
1339        pi_implicit(
1340            "ρ",
1341            type0(),
1342            pi_implicit(
1343                "m",
1344                type0(),
1345                pi_implicit(
1346                    "α",
1347                    type0(),
1348                    pi(
1349                        bvar(0),
1350                        app(app(app(var("ReaderT"), bvar(3)), bvar(2)), bvar(1)),
1351                    ),
1352                ),
1353            ),
1354        ),
1355    );
1356    b.axiom(
1357        "ReaderT.ask",
1358        pi_implicit(
1359            "ρ",
1360            type0(),
1361            pi_implicit(
1362                "m",
1363                type0(),
1364                app(app(app(var("ReaderT"), bvar(1)), bvar(0)), bvar(1)),
1365            ),
1366        ),
1367    );
1368    b.axiom(
1369        "ReaderT.run",
1370        pi_implicit(
1371            "ρ",
1372            type0(),
1373            pi_implicit(
1374                "m",
1375                type0(),
1376                pi_implicit(
1377                    "α",
1378                    type0(),
1379                    pi(
1380                        app(app(app(var("ReaderT"), bvar(2)), bvar(1)), bvar(0)),
1381                        pi(bvar(3), bvar(3)),
1382                    ),
1383                ),
1384            ),
1385        ),
1386    );
1387    b.axiom(
1388        "ReaderT.bind",
1389        pi_implicit(
1390            "ρ",
1391            type0(),
1392            pi_implicit(
1393                "m",
1394                type0(),
1395                pi_implicit(
1396                    "α",
1397                    type0(),
1398                    pi_implicit(
1399                        "β",
1400                        type0(),
1401                        pi(
1402                            app(app(app(var("ReaderT"), bvar(3)), bvar(2)), bvar(1)),
1403                            pi(
1404                                pi(
1405                                    bvar(2),
1406                                    app(app(app(var("ReaderT"), bvar(4)), bvar(3)), bvar(1)),
1407                                ),
1408                                app(app(app(var("ReaderT"), bvar(4)), bvar(3)), bvar(1)),
1409                            ),
1410                        ),
1411                    ),
1412                ),
1413            ),
1414        ),
1415    );
1416}
1417/// Add `WriterT` monad transformer.
1418#[allow(dead_code)]
1419pub fn add_writer_monad(b: &mut EnvBuilder) {
1420    b.axiom("WriterT", pi(type0(), pi(type0(), pi(type0(), type0()))));
1421    b.axiom(
1422        "WriterT.pure",
1423        pi_implicit(
1424            "ω",
1425            type0(),
1426            pi_implicit(
1427                "m",
1428                type0(),
1429                pi_implicit(
1430                    "α",
1431                    type0(),
1432                    pi(
1433                        bvar(0),
1434                        app(app(app(var("WriterT"), bvar(3)), bvar(2)), bvar(1)),
1435                    ),
1436                ),
1437            ),
1438        ),
1439    );
1440    b.axiom(
1441        "WriterT.tell",
1442        pi_implicit(
1443            "ω",
1444            type0(),
1445            pi_implicit(
1446                "m",
1447                type0(),
1448                pi(
1449                    bvar(1),
1450                    app(app(app(var("WriterT"), bvar(2)), bvar(1)), var("Unit")),
1451                ),
1452            ),
1453        ),
1454    );
1455    b.axiom(
1456        "WriterT.listen",
1457        pi_implicit(
1458            "ω",
1459            type0(),
1460            pi_implicit(
1461                "m",
1462                type0(),
1463                pi_implicit(
1464                    "α",
1465                    type0(),
1466                    pi(
1467                        app(app(app(var("WriterT"), bvar(2)), bvar(1)), bvar(0)),
1468                        app(
1469                            app(app(var("WriterT"), bvar(3)), bvar(2)),
1470                            app(app(var("Prod"), bvar(1)), bvar(3)),
1471                        ),
1472                    ),
1473                ),
1474            ),
1475        ),
1476    );
1477}
1478/// Add `ContT` continuation monad transformer.
1479#[allow(dead_code)]
1480pub fn add_cont_monad(b: &mut EnvBuilder) {
1481    b.axiom("ContT", pi(type0(), pi(type0(), pi(type0(), type0()))));
1482    b.axiom(
1483        "ContT.pure",
1484        pi_implicit(
1485            "r",
1486            type0(),
1487            pi_implicit(
1488                "m",
1489                type0(),
1490                pi_implicit(
1491                    "α",
1492                    type0(),
1493                    pi(
1494                        bvar(0),
1495                        app(app(app(var("ContT"), bvar(3)), bvar(2)), bvar(1)),
1496                    ),
1497                ),
1498            ),
1499        ),
1500    );
1501    b.axiom(
1502        "ContT.callCC",
1503        pi_implicit(
1504            "r",
1505            type0(),
1506            pi_implicit(
1507                "m",
1508                type0(),
1509                pi_implicit(
1510                    "α",
1511                    type0(),
1512                    pi(
1513                        pi(
1514                            pi(
1515                                bvar(0),
1516                                app(app(app(var("ContT"), bvar(3)), bvar(2)), bvar(1)),
1517                            ),
1518                            app(app(app(var("ContT"), bvar(3)), bvar(2)), bvar(1)),
1519                        ),
1520                        app(app(app(var("ContT"), bvar(3)), bvar(2)), bvar(1)),
1521                    ),
1522                ),
1523            ),
1524        ),
1525    );
1526}
1527/// Add `ExceptT` monad transformer.
1528#[allow(dead_code)]
1529pub fn add_except_monad(b: &mut EnvBuilder) {
1530    b.axiom("ExceptT", pi(type0(), pi(type0(), pi(type0(), type0()))));
1531    b.axiom(
1532        "ExceptT.pure",
1533        pi_implicit(
1534            "ε",
1535            type0(),
1536            pi_implicit(
1537                "m",
1538                type0(),
1539                pi_implicit(
1540                    "α",
1541                    type0(),
1542                    pi(
1543                        bvar(0),
1544                        app(app(app(var("ExceptT"), bvar(3)), bvar(2)), bvar(1)),
1545                    ),
1546                ),
1547            ),
1548        ),
1549    );
1550    b.axiom(
1551        "ExceptT.throw",
1552        pi_implicit(
1553            "ε",
1554            type0(),
1555            pi_implicit(
1556                "m",
1557                type0(),
1558                pi_implicit(
1559                    "α",
1560                    type0(),
1561                    pi(
1562                        bvar(2),
1563                        app(app(app(var("ExceptT"), bvar(3)), bvar(2)), bvar(1)),
1564                    ),
1565                ),
1566            ),
1567        ),
1568    );
1569    b.axiom(
1570        "ExceptT.catch",
1571        pi_implicit(
1572            "ε",
1573            type0(),
1574            pi_implicit(
1575                "m",
1576                type0(),
1577                pi_implicit(
1578                    "α",
1579                    type0(),
1580                    pi(
1581                        app(app(app(var("ExceptT"), bvar(2)), bvar(1)), bvar(0)),
1582                        pi(
1583                            pi(
1584                                bvar(3),
1585                                app(app(app(var("ExceptT"), bvar(4)), bvar(3)), bvar(2)),
1586                            ),
1587                            app(app(app(var("ExceptT"), bvar(4)), bvar(3)), bvar(2)),
1588                        ),
1589                    ),
1590                ),
1591            ),
1592        ),
1593    );
1594}
1595/// Add `Vector` (length-indexed array).
1596#[allow(dead_code)]
1597pub fn add_vector(b: &mut EnvBuilder) {
1598    b.axiom("Vector", pi(type0(), pi(var("Nat"), type0())));
1599    b.axiom(
1600        "Vector.nil",
1601        pi_implicit(
1602            "α",
1603            type0(),
1604            app(app(var("Vector"), bvar(0)), var("Nat.zero")),
1605        ),
1606    );
1607    b.axiom(
1608        "Vector.cons",
1609        pi_implicit(
1610            "α",
1611            type0(),
1612            pi_implicit(
1613                "n",
1614                var("Nat"),
1615                pi(
1616                    bvar(1),
1617                    pi(
1618                        app(app(var("Vector"), bvar(2)), bvar(1)),
1619                        app(app(var("Vector"), bvar(3)), app(var("Nat.succ"), bvar(2))),
1620                    ),
1621                ),
1622            ),
1623        ),
1624    );
1625    b.axiom(
1626        "Vector.head",
1627        pi_implicit(
1628            "α",
1629            type0(),
1630            pi_implicit(
1631                "n",
1632                var("Nat"),
1633                pi(
1634                    app(app(var("Vector"), bvar(1)), app(var("Nat.succ"), bvar(0))),
1635                    bvar(2),
1636                ),
1637            ),
1638        ),
1639    );
1640    b.axiom(
1641        "Vector.tail",
1642        pi_implicit(
1643            "α",
1644            type0(),
1645            pi_implicit(
1646                "n",
1647                var("Nat"),
1648                pi(
1649                    app(app(var("Vector"), bvar(1)), app(var("Nat.succ"), bvar(0))),
1650                    app(app(var("Vector"), bvar(2)), bvar(1)),
1651                ),
1652            ),
1653        ),
1654    );
1655    b.axiom(
1656        "Vector.get",
1657        pi_implicit(
1658            "α",
1659            type0(),
1660            pi_implicit(
1661                "n",
1662                var("Nat"),
1663                pi(
1664                    app(app(var("Vector"), bvar(1)), bvar(0)),
1665                    pi(var("Nat"), bvar(2)),
1666                ),
1667            ),
1668        ),
1669    );
1670    b.axiom(
1671        "Vector.map",
1672        pi_implicit(
1673            "α",
1674            type0(),
1675            pi_implicit(
1676                "β",
1677                type0(),
1678                pi_implicit(
1679                    "n",
1680                    var("Nat"),
1681                    pi(
1682                        pi(bvar(2), bvar(2)),
1683                        pi(
1684                            app(app(var("Vector"), bvar(3)), bvar(1)),
1685                            app(app(var("Vector"), bvar(3)), bvar(2)),
1686                        ),
1687                    ),
1688                ),
1689            ),
1690        ),
1691    );
1692    b.axiom(
1693        "Vector.append",
1694        pi_implicit(
1695            "α",
1696            type0(),
1697            pi_implicit(
1698                "m",
1699                var("Nat"),
1700                pi_implicit(
1701                    "n",
1702                    var("Nat"),
1703                    pi(
1704                        app(app(var("Vector"), bvar(2)), bvar(1)),
1705                        pi(
1706                            app(app(var("Vector"), bvar(3)), bvar(1)),
1707                            app(
1708                                app(var("Vector"), bvar(4)),
1709                                app(app(var("Nat.add"), bvar(3)), bvar(2)),
1710                            ),
1711                        ),
1712                    ),
1713                ),
1714            ),
1715        ),
1716    );
1717    b.axiom(
1718        "Vector.reverse",
1719        pi_implicit(
1720            "α",
1721            type0(),
1722            pi_implicit(
1723                "n",
1724                var("Nat"),
1725                pi(
1726                    app(app(var("Vector"), bvar(1)), bvar(0)),
1727                    app(app(var("Vector"), bvar(2)), bvar(1)),
1728                ),
1729            ),
1730        ),
1731    );
1732    b.axiom(
1733        "Vector.foldl",
1734        pi_implicit(
1735            "α",
1736            type0(),
1737            pi_implicit(
1738                "β",
1739                type0(),
1740                pi_implicit(
1741                    "n",
1742                    var("Nat"),
1743                    pi(
1744                        bvar(1),
1745                        pi(
1746                            pi(bvar(2), pi(bvar(3), bvar(3))),
1747                            pi(app(app(var("Vector"), bvar(3)), bvar(1)), bvar(3)),
1748                        ),
1749                    ),
1750                ),
1751            ),
1752        ),
1753    );
1754}
1755/// Add `Quotient` type.
1756#[allow(dead_code)]
1757pub fn add_quotient(b: &mut EnvBuilder) {
1758    b.axiom("Setoid", pi(type0(), type1()));
1759    b.axiom(
1760        "Quotient",
1761        pi_implicit("α", type0(), pi(app(var("Setoid"), bvar(0)), type0())),
1762    );
1763    b.axiom(
1764        "Quotient.mk",
1765        pi_implicit(
1766            "α",
1767            type0(),
1768            pi_implicit(
1769                "s",
1770                app(var("Setoid"), bvar(0)),
1771                pi(bvar(1), app(app(var("Quotient"), bvar(2)), bvar(1))),
1772            ),
1773        ),
1774    );
1775    b.axiom(
1776        "Quotient.lift",
1777        pi_implicit(
1778            "α",
1779            type0(),
1780            pi_implicit(
1781                "s",
1782                app(var("Setoid"), bvar(0)),
1783                pi_implicit(
1784                    "β",
1785                    type0(),
1786                    pi(
1787                        pi(bvar(2), bvar(1)),
1788                        pi(
1789                            pi_implicit(
1790                                "a",
1791                                bvar(3),
1792                                pi_implicit(
1793                                    "b",
1794                                    bvar(4),
1795                                    pi(
1796                                        prop(),
1797                                        app(
1798                                            app(var("Eq"), app(bvar(5), bvar(2))),
1799                                            app(bvar(5), bvar(1)),
1800                                        ),
1801                                    ),
1802                                ),
1803                            ),
1804                            pi(app(app(var("Quotient"), bvar(4)), bvar(3)), bvar(2)),
1805                        ),
1806                    ),
1807                ),
1808            ),
1809        ),
1810    );
1811    b.axiom(
1812        "Quotient.sound",
1813        pi_implicit(
1814            "α",
1815            type0(),
1816            pi_implicit(
1817                "s",
1818                app(var("Setoid"), bvar(0)),
1819                pi_implicit(
1820                    "a",
1821                    bvar(1),
1822                    pi_implicit(
1823                        "b",
1824                        bvar(2),
1825                        pi(
1826                            prop(),
1827                            app(
1828                                app(var("Eq"), app(app(var("Quotient.mk"), bvar(3)), bvar(2))),
1829                                app(app(var("Quotient.mk"), bvar(3)), bvar(1)),
1830                            ),
1831                        ),
1832                    ),
1833                ),
1834            ),
1835        ),
1836    );
1837}
1838/// Add `Functor`, `Applicative`, `Monad`, `Ord`, `BEq`, `Hashable`, `ToString` type classes.
1839#[allow(dead_code)]
1840pub fn add_type_classes(b: &mut EnvBuilder) {
1841    if !b.contains("Functor") {
1842        add_functor(b);
1843    }
1844    if !b.contains("Monad") {
1845        add_monad(b);
1846    }
1847    // Monad.bind : {M : Type → Type} → [Monad M] → {α β : Type} → M α → (α → M β) → M β
1848    if !b.contains("Monad.bind") {
1849        let bind_ty = pi_implicit(
1850            "M",
1851            pi(type0(), type0()),
1852            pi_inst(
1853                "_",
1854                app(var("Monad"), bvar(0)),
1855                pi_implicit(
1856                    "α",
1857                    type0(),
1858                    pi_implicit(
1859                        "β",
1860                        type0(),
1861                        pi(
1862                            app(bvar(4), bvar(1)),
1863                            pi(pi(bvar(2), app(bvar(5), bvar(2))), app(bvar(5), bvar(2))),
1864                        ),
1865                    ),
1866                ),
1867            ),
1868        );
1869        b.axiom("Monad.bind", bind_ty);
1870    }
1871    b.axiom("Applicative", pi(pi(type0(), type0()), prop()));
1872    b.axiom("Foldable", pi(pi(type0(), type0()), prop()));
1873    b.axiom("Traversable", pi(pi(type0(), type0()), prop()));
1874    b.axiom("Ord", pi(type0(), prop()));
1875    b.axiom(
1876        "Ord.compare",
1877        pi_implicit(
1878            "α",
1879            type0(),
1880            pi(
1881                app(var("Ord"), bvar(0)),
1882                pi(bvar(1), pi(bvar(2), var("Ordering"))),
1883            ),
1884        ),
1885    );
1886    b.axiom("Hashable", pi(type0(), prop()));
1887    b.axiom(
1888        "Hashable.hash",
1889        pi_implicit(
1890            "α",
1891            type0(),
1892            pi(app(var("Hashable"), bvar(0)), pi(bvar(1), var("Nat"))),
1893        ),
1894    );
1895    b.axiom("BEq", pi(type0(), prop()));
1896    b.axiom(
1897        "BEq.beq",
1898        pi_implicit(
1899            "α",
1900            type0(),
1901            pi(
1902                app(var("BEq"), bvar(0)),
1903                pi(bvar(1), pi(bvar(2), var("Bool"))),
1904            ),
1905        ),
1906    );
1907    b.axiom("ToString", pi(type0(), prop()));
1908    b.axiom(
1909        "ToString.toString",
1910        pi_implicit(
1911            "α",
1912            type0(),
1913            pi(app(var("ToString"), bvar(0)), pi(bvar(1), var("String"))),
1914        ),
1915    );
1916    b.axiom("Repr", pi(type0(), prop()));
1917    if !b.contains("Format") {
1918        b.axiom("Format", type0());
1919    }
1920    b.axiom(
1921        "Repr.reprPrec",
1922        pi_implicit(
1923            "α",
1924            type0(),
1925            pi(
1926                app(var("Repr"), bvar(0)),
1927                pi(bvar(1), pi(var("Nat"), var("Format"))),
1928            ),
1929        ),
1930    );
1931}
1932/// Add `Ordering` type and helpers.
1933#[allow(dead_code)]
1934pub fn add_ordering(b: &mut EnvBuilder) {
1935    b.axiom("Ordering", type0());
1936    b.axiom("Ordering.lt", var("Ordering"));
1937    b.axiom("Ordering.eq", var("Ordering"));
1938    b.axiom("Ordering.gt", var("Ordering"));
1939    b.axiom("Ordering.swap", pi(var("Ordering"), var("Ordering")));
1940    b.axiom("Ordering.isLT", pi(var("Ordering"), var("Bool")));
1941    b.axiom("Ordering.isEQ", pi(var("Ordering"), var("Bool")));
1942    b.axiom("Ordering.isGT", pi(var("Ordering"), var("Bool")));
1943    b.axiom(
1944        "compareOfLessAndEq",
1945        pi_implicit(
1946            "α",
1947            type0(),
1948            pi(
1949                app(var("Ord"), bvar(0)),
1950                pi(bvar(1), pi(bvar(2), var("Ordering"))),
1951            ),
1952        ),
1953    );
1954}
1955/// Add `Format` pretty-printing combinators.
1956#[allow(dead_code)]
1957pub fn add_format(b: &mut EnvBuilder) {
1958    if !b.contains("Format") {
1959        b.axiom("Format", type0());
1960    }
1961    b.axiom("Format.nil", var("Format"));
1962    b.axiom("Format.text", pi(var("String"), var("Format")));
1963    b.axiom("Format.line", var("Format"));
1964    b.axiom(
1965        "Format.nest",
1966        pi(var("Nat"), pi(var("Format"), var("Format"))),
1967    );
1968    b.axiom("Format.group", pi(var("Format"), var("Format")));
1969    b.axiom(
1970        "Format.append",
1971        pi(var("Format"), pi(var("Format"), var("Format"))),
1972    );
1973    b.axiom(
1974        "Format.join",
1975        pi(app(var("List"), var("Format")), var("Format")),
1976    );
1977    b.axiom(
1978        "Format.pretty",
1979        pi(var("Format"), pi(var("Nat"), var("String"))),
1980    );
1981    b.axiom("Format.indentD", pi(var("Format"), var("Format")));
1982    b.axiom(
1983        "Format.bracket",
1984        pi(
1985            var("String"),
1986            pi(var("Format"), pi(var("String"), var("Format"))),
1987        ),
1988    );
1989}
1990/// Add `RBTree` (red-black tree).
1991#[allow(dead_code)]
1992pub fn add_rb_tree(b: &mut EnvBuilder) {
1993    if !b.contains("Ord") {
1994        b.axiom("Ord", pi(type0(), prop()));
1995    }
1996    b.axiom("RBTree", pi(type0(), type1()));
1997    b.axiom(
1998        "RBTree.empty",
1999        pi_implicit(
2000            "α",
2001            type0(),
2002            pi(app(var("Ord"), bvar(0)), app(var("RBTree"), bvar(1))),
2003        ),
2004    );
2005    b.axiom(
2006        "RBTree.insert",
2007        pi_implicit(
2008            "α",
2009            type0(),
2010            pi(
2011                app(var("Ord"), bvar(0)),
2012                pi(
2013                    bvar(1),
2014                    pi(app(var("RBTree"), bvar(2)), app(var("RBTree"), bvar(3))),
2015                ),
2016            ),
2017        ),
2018    );
2019    b.axiom(
2020        "RBTree.find",
2021        pi_implicit(
2022            "α",
2023            type0(),
2024            pi(
2025                app(var("Ord"), bvar(0)),
2026                pi(
2027                    bvar(1),
2028                    pi(app(var("RBTree"), bvar(2)), app(var("Option"), bvar(3))),
2029                ),
2030            ),
2031        ),
2032    );
2033    b.axiom(
2034        "RBTree.contains",
2035        pi_implicit(
2036            "α",
2037            type0(),
2038            pi(
2039                app(var("Ord"), bvar(0)),
2040                pi(bvar(1), pi(app(var("RBTree"), bvar(2)), var("Bool"))),
2041            ),
2042        ),
2043    );
2044    b.axiom(
2045        "RBTree.erase",
2046        pi_implicit(
2047            "α",
2048            type0(),
2049            pi(
2050                app(var("Ord"), bvar(0)),
2051                pi(
2052                    bvar(1),
2053                    pi(app(var("RBTree"), bvar(2)), app(var("RBTree"), bvar(3))),
2054                ),
2055            ),
2056        ),
2057    );
2058    b.axiom(
2059        "RBTree.size",
2060        pi_implicit(
2061            "α",
2062            type0(),
2063            pi_implicit(
2064                "_",
2065                app(var("Ord"), bvar(0)),
2066                pi(app(var("RBTree"), bvar(1)), var("Nat")),
2067            ),
2068        ),
2069    );
2070    b.axiom(
2071        "RBTree.toList",
2072        pi_implicit(
2073            "α",
2074            type0(),
2075            pi_implicit(
2076                "_",
2077                app(var("Ord"), bvar(0)),
2078                pi(app(var("RBTree"), bvar(1)), app(var("List"), bvar(2))),
2079            ),
2080        ),
2081    );
2082    b.axiom(
2083        "RBTree.fromList",
2084        pi_implicit(
2085            "α",
2086            type0(),
2087            pi(
2088                app(var("Ord"), bvar(0)),
2089                pi(app(var("List"), bvar(1)), app(var("RBTree"), bvar(2))),
2090            ),
2091        ),
2092    );
2093}
oxilean_std/env_builder/functions.rs

oxilean_std/env_builder/
functions.rs
