oxilean_std/lambda_calculus/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::Node;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8use super::types::{
9    AlphaEquivalenceChecker, BetaReducer, BinarySession, Context, LinearTypeChecker,
10    SessionTypeCompatibility, SimpleType, Strategy, Term, TypeInferenceSystem,
11};
12
13pub fn app(f: Expr, a: Expr) -> Expr {
14    Expr::App(Node::new(f), Node::new(a))
15}
16pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
17    app(app(f, a), b)
18}
19pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
20    app(app2(f, a, b), c)
21}
22pub fn cst(s: &str) -> Expr {
23    Expr::Const(Name::str(s), vec![])
24}
25pub fn prop() -> Expr {
26    Expr::Sort(Level::zero())
27}
28pub fn type0() -> Expr {
29    Expr::Sort(Level::succ(Level::zero()))
30}
31pub fn type1() -> Expr {
32    Expr::Sort(Level::succ(Level::succ(Level::zero())))
33}
34pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
35    Expr::Pi(bi, Name::str(name), Node::new(dom), Node::new(body))
36}
37pub fn arrow(a: Expr, b: Expr) -> Expr {
38    pi(BinderInfo::Default, "_", a, b)
39}
40pub fn impl_pi(name: &str, dom: Expr, body: Expr) -> Expr {
41    pi(BinderInfo::Implicit, name, dom, body)
42}
43pub fn bvar(n: u32) -> Expr {
44    Expr::BVar(n)
45}
46pub fn nat_ty() -> Expr {
47    cst("Nat")
48}
49pub fn bool_ty() -> Expr {
50    cst("Bool")
51}
52pub fn list_ty(elem: Expr) -> Expr {
53    app(cst("List"), elem)
54}
55pub fn option_ty(elem: Expr) -> Expr {
56    app(cst("Option"), elem)
57}
58/// UntypedTerm: the type of untyped lambda terms (de Bruijn representation)
59pub fn untyped_term_ty() -> Expr {
60    type0()
61}
62/// Variable: de Bruijn index n refers to the n-th enclosing binder
63pub fn variable_ty() -> Expr {
64    arrow(nat_ty(), untyped_term_ty())
65}
66/// Abstraction: λ.t (binder in de Bruijn — no variable name needed)
67pub fn abstraction_ty() -> Expr {
68    arrow(untyped_term_ty(), untyped_term_ty())
69}
70/// Application: t s
71pub fn application_ty() -> Expr {
72    arrow(
73        untyped_term_ty(),
74        arrow(untyped_term_ty(), untyped_term_ty()),
75    )
76}
77/// Substitution: t[s/n] — substitute s for de Bruijn index n in t
78pub fn substitution_ty() -> Expr {
79    arrow(
80        untyped_term_ty(),
81        arrow(untyped_term_ty(), arrow(nat_ty(), untyped_term_ty())),
82    )
83}
84/// BetaRedex: t is a beta redex iff t = (λ.s) u
85pub fn beta_redex_ty() -> Expr {
86    arrow(untyped_term_ty(), prop())
87}
88/// EtaRedex: t is an eta redex iff t = λ.(s (BVar 0)) with BVar 0 not free in s
89pub fn eta_redex_ty() -> Expr {
90    arrow(untyped_term_ty(), prop())
91}
92/// BetaStep: one-step β-reduction t →β s
93pub fn beta_step_ty() -> Expr {
94    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
95}
96/// EtaStep: one-step η-reduction t →η s
97pub fn eta_step_ty() -> Expr {
98    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
99}
100/// BetaReduction: reflexive transitive closure of →β
101pub fn beta_reduction_ty() -> Expr {
102    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
103}
104/// BetaEquiv: β-equivalence (=β)
105pub fn beta_equiv_ty() -> Expr {
106    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
107}
108/// NormalForm: t has no β-redex
109pub fn normal_form_ty() -> Expr {
110    arrow(untyped_term_ty(), prop())
111}
112/// WeakNormalForm: t can be reduced to a normal form
113pub fn weak_normal_form_ty() -> Expr {
114    arrow(untyped_term_ty(), prop())
115}
116/// HeadNormalForm: the head of t is not a redex
117pub fn head_normal_form_ty() -> Expr {
118    arrow(untyped_term_ty(), prop())
119}
120/// ChurchNumeral: the Church encoding of n as λf.λx.f^n x
121pub fn church_numeral_ty() -> Expr {
122    arrow(nat_ty(), untyped_term_ty())
123}
124/// ChurchSucc: the successor combinator S = λn.λf.λx.f (n f x)
125pub fn church_succ_ty() -> Expr {
126    untyped_term_ty()
127}
128/// ChurchPlus: addition combinator M = λm.λn.λf.λx.m f (n f x)
129pub fn church_plus_ty() -> Expr {
130    untyped_term_ty()
131}
132/// ChurchMul: multiplication combinator M = λm.λn.λf.m (n f)
133pub fn church_mul_ty() -> Expr {
134    untyped_term_ty()
135}
136/// ChurchExp: exponentiation combinator E = λm.λn.n m
137pub fn church_exp_ty() -> Expr {
138    untyped_term_ty()
139}
140/// ChurchPred: predecessor combinator (Kleene encoding)
141pub fn church_pred_ty() -> Expr {
142    untyped_term_ty()
143}
144/// ChurchIsZero: test whether a Church numeral is zero
145pub fn church_is_zero_ty() -> Expr {
146    arrow(untyped_term_ty(), bool_ty())
147}
148/// ChurchNumeralCorrect: church_numeral n reduces to the standard encoding
149pub fn church_numeral_correct_ty() -> Expr {
150    arrow(nat_ty(), prop())
151}
152/// ChurchArithCorrect: Church arithmetic is correct w.r.t. Nat arithmetic
153pub fn church_arith_correct_ty() -> Expr {
154    prop()
155}
156/// YCombinator: Curry's Y = λf.(λx.f(x x))(λx.f(x x))
157pub fn y_combinator_ty() -> Expr {
158    untyped_term_ty()
159}
160/// TuringCombinator: Turing's Θ fixed point combinator
161pub fn turing_combinator_ty() -> Expr {
162    untyped_term_ty()
163}
164/// RecursionTheorem: every function has a fixed point
165pub fn recursion_theorem_ty() -> Expr {
166    arrow(arrow(untyped_term_ty(), untyped_term_ty()), prop())
167}
168/// YFixedPoint: Y f =β f (Y f)
169pub fn y_fixed_point_ty() -> Expr {
170    arrow(untyped_term_ty(), prop())
171}
172/// OmegaCombinator: Ω = (λx.x x)(λx.x x) — diverging term
173pub fn omega_combinator_ty() -> Expr {
174    untyped_term_ty()
175}
176/// OmegaDiverges: Ω has no normal form
177pub fn omega_diverges_ty() -> Expr {
178    prop()
179}
180/// NormalOrderRedex: leftmost-outermost redex
181pub fn normal_order_redex_ty() -> Expr {
182    arrow(untyped_term_ty(), option_ty(untyped_term_ty()))
183}
184/// ApplicativeOrderRedex: leftmost-innermost redex (call by value)
185pub fn applicative_order_redex_ty() -> Expr {
186    arrow(untyped_term_ty(), option_ty(untyped_term_ty()))
187}
188/// HeadReduction: reduce the head redex (lazy evaluation)
189pub fn head_reduction_ty() -> Expr {
190    arrow(untyped_term_ty(), option_ty(untyped_term_ty()))
191}
192/// NormalOrderStrategy: normal order finds normal form if one exists
193pub fn normal_order_strategy_ty() -> Expr {
194    prop()
195}
196/// StandardizationTheorem: if t has a normal form, normal order reaches it
197pub fn standardization_theorem_ty() -> Expr {
198    prop()
199}
200/// CallByValueReduction: strict/CBV evaluation
201pub fn cbv_reduction_ty() -> Expr {
202    arrow(untyped_term_ty(), option_ty(untyped_term_ty()))
203}
204/// CallByNeedReduction: lazy/sharing evaluation
205pub fn cbn_reduction_ty() -> Expr {
206    arrow(untyped_term_ty(), option_ty(untyped_term_ty()))
207}
208/// DiamondProperty: if t →₁ u and t →₁ v then ∃ w, u →₁ w and v →₁ w
209pub fn diamond_property_ty() -> Expr {
210    pi(
211        BinderInfo::Default,
212        "t",
213        untyped_term_ty(),
214        pi(
215            BinderInfo::Default,
216            "u",
217            untyped_term_ty(),
218            pi(BinderInfo::Default, "v", untyped_term_ty(), prop()),
219        ),
220    )
221}
222/// ChurchRosserTheorem: β-reduction is confluent
223pub fn church_rosser_theorem_ty() -> Expr {
224    prop()
225}
226/// Confluence: the reflexive transitive closure of →β has the diamond property
227pub fn confluence_ty() -> Expr {
228    prop()
229}
230/// ParallelReduction: parallel β-reduction (β∥) — key for CR proof
231pub fn parallel_reduction_ty() -> Expr {
232    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
233}
234/// ParallelReductionComplete: t →β s implies t →β∥ s
235pub fn parallel_reduction_complete_ty() -> Expr {
236    prop()
237}
238/// ParallelMaxReduct: complete parallel development
239pub fn parallel_max_reduct_ty() -> Expr {
240    arrow(untyped_term_ty(), untyped_term_ty())
241}
242/// ParallelMaxReductProperty: diamond property for complete development
243pub fn parallel_max_reduct_property_ty() -> Expr {
244    prop()
245}
246/// BohmTree: the Böhm tree of a lambda term (possibly infinite)
247pub fn bohm_tree_ty() -> Expr {
248    type0()
249}
250/// BohmTreeOf: compute the Böhm tree of a term
251pub fn bohm_tree_of_ty() -> Expr {
252    arrow(untyped_term_ty(), bohm_tree_ty())
253}
254/// UnsolvableTerm: a term with no head normal form
255pub fn unsolvable_term_ty() -> Expr {
256    arrow(untyped_term_ty(), prop())
257}
258/// SolvableTerm: a term with a head normal form
259pub fn solvable_term_ty() -> Expr {
260    arrow(untyped_term_ty(), prop())
261}
262/// BohmEquiv: two terms are Böhm-equal iff their Böhm trees are equal
263pub fn bohm_equiv_ty() -> Expr {
264    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
265}
266/// ObservationalEquiv: contextual equivalence in the untyped λ-calculus
267pub fn observational_equiv_ty() -> Expr {
268    arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop()))
269}
270/// BohmTheorem: two distinct β-normal forms are separable by a context
271pub fn bohm_theorem_ty() -> Expr {
272    prop()
273}
274/// SimpleType: the type of simple types over a base type set
275pub fn simple_type_ty() -> Expr {
276    type0()
277}
278/// BaseType: a ground/atomic type
279pub fn base_type_ty() -> Expr {
280    arrow(type0(), simple_type_ty())
281}
282/// ArrowType: function type A → B in simple type theory
283pub fn arrow_type_ty() -> Expr {
284    arrow(simple_type_ty(), arrow(simple_type_ty(), simple_type_ty()))
285}
286/// TypingContext: a finite map from variables to simple types
287pub fn typing_context_ty() -> Expr {
288    type0()
289}
290/// STLCTyping: Γ ⊢ t : τ (simple type assignment)
291pub fn stlc_typing_ty() -> Expr {
292    arrow(
293        typing_context_ty(),
294        arrow(untyped_term_ty(), arrow(simple_type_ty(), prop())),
295    )
296}
297/// STLCSubjectReduction: if Γ ⊢ t : τ and t →β s then Γ ⊢ s : τ
298pub fn stlc_subject_reduction_ty() -> Expr {
299    prop()
300}
301/// STLCStrongNormalization: all well-typed STLC terms are strongly normalizing
302pub fn stlc_strong_normalization_ty() -> Expr {
303    prop()
304}
305/// STLCChurchRosser: STLC β-reduction is confluent
306pub fn stlc_church_rosser_ty() -> Expr {
307    prop()
308}
309/// STLCDecidability: type-checking STLC is decidable
310pub fn stlc_decidability_ty() -> Expr {
311    prop()
312}
313/// SystemFType: types of System F (including type variables and ∀)
314pub fn system_f_type_ty() -> Expr {
315    type0()
316}
317/// SystemFTerm: terms of System F (including type abstraction and application)
318pub fn system_f_term_ty() -> Expr {
319    type0()
320}
321/// SystemFTyping: typing judgment for System F
322pub fn system_f_typing_ty() -> Expr {
323    arrow(
324        typing_context_ty(),
325        arrow(system_f_term_ty(), arrow(system_f_type_ty(), prop())),
326    )
327}
328/// SystemFStrongNormalization: System F is strongly normalizing
329pub fn system_f_sn_ty() -> Expr {
330    prop()
331}
332/// SystemFConfluence: System F β-reduction is confluent
333pub fn system_f_confluence_ty() -> Expr {
334    prop()
335}
336/// SystemFParametricity: Reynolds's abstraction theorem
337pub fn system_f_parametricity_ty() -> Expr {
338    prop()
339}
340/// SystemFUndecidableTyping: type inference for System F is undecidable (Wells)
341pub fn system_f_undecidable_ty() -> Expr {
342    prop()
343}
344/// ChurchEncoding_NatF: System F encoding of natural numbers
345/// ∀ α. (α → α) → α → α
346pub fn church_nat_f_ty() -> Expr {
347    system_f_type_ty()
348}
349/// ChurchEncoding_BoolF: System F encoding of booleans
350/// ∀ α. α → α → α
351pub fn church_bool_f_ty() -> Expr {
352    system_f_type_ty()
353}
354/// ChurchEncoding_ListF: System F encoding of lists
355/// ∀ α β. β → (α → β → β) → β
356pub fn church_list_f_ty() -> Expr {
357    system_f_type_ty()
358}
359/// Kind: the kind language of System Fω (* and →)
360pub fn kind_ty() -> Expr {
361    type0()
362}
363/// StarKind: the base kind *
364pub fn star_kind_ty() -> Expr {
365    kind_ty()
366}
367/// KindArrow: kind constructor A ⇒ B
368pub fn kind_arrow_ty() -> Expr {
369    arrow(kind_ty(), arrow(kind_ty(), kind_ty()))
370}
371/// TypeConstructor: a type-level function with a kind
372pub fn type_constructor_ty() -> Expr {
373    type0()
374}
375/// SystemFOmegaType: types of System Fω
376pub fn system_fomega_type_ty() -> Expr {
377    type0()
378}
379/// SystemFOmegaTerm: terms of System Fω
380pub fn system_fomega_term_ty() -> Expr {
381    type0()
382}
383/// SystemFOmegaTyping: typing judgment for Fω
384pub fn system_fomega_typing_ty() -> Expr {
385    arrow(
386        typing_context_ty(),
387        arrow(
388            system_fomega_term_ty(),
389            arrow(system_fomega_type_ty(), prop()),
390        ),
391    )
392}
393/// SystemFOmegaSN: Fω is strongly normalizing
394pub fn system_fomega_sn_ty() -> Expr {
395    prop()
396}
397/// SystemFOmegaKindSoundness: well-kinded types have sound interpretations
398pub fn system_fomega_kind_soundness_ty() -> Expr {
399    prop()
400}
401/// PTS_Axiom: the set of axioms (s : s') for a pure type system
402pub fn pts_axiom_ty() -> Expr {
403    type0()
404}
405/// PTS_Rule: the set of rules (s₁, s₂, s₃) for Π-type formation
406pub fn pts_rule_ty() -> Expr {
407    type0()
408}
409/// PureTypeSystem: a PTS defined by sorts S, axioms A, rules R
410pub fn pure_type_system_ty() -> Expr {
411    type0()
412}
413/// PTSTyping: Γ ⊢ t : T in a PTS
414pub fn pts_typing_ty() -> Expr {
415    arrow(
416        pure_type_system_ty(),
417        arrow(
418            typing_context_ty(),
419            arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop())),
420        ),
421    )
422}
423/// CoC: the Calculus of Constructions (top of the λ-cube)
424pub fn coc_ty() -> Expr {
425    pure_type_system_ty()
426}
427/// LambdaArrow: simply-typed lambda calculus corner of cube
428pub fn lambda_arrow_ty() -> Expr {
429    pure_type_system_ty()
430}
431/// Lambda2: System F corner of cube (type polymorphism)
432pub fn lambda2_ty() -> Expr {
433    pure_type_system_ty()
434}
435/// LambdaOmega: System Fω corner (type constructors)
436pub fn lambda_omega_ty() -> Expr {
437    pure_type_system_ty()
438}
439/// LambdaP: λP (dependent types, Edinburgh LF)
440pub fn lambda_p_ty() -> Expr {
441    pure_type_system_ty()
442}
443/// PTSSubjectReduction: subject reduction holds for all functional PTS
444pub fn pts_subject_reduction_ty() -> Expr {
445    arrow(pure_type_system_ty(), prop())
446}
447/// PTSConfluence: confluence holds for all PTS (β-reduction)
448pub fn pts_confluence_ty() -> Expr {
449    arrow(pure_type_system_ty(), prop())
450}
451/// CoCStrongNormalization: the Calculus of Constructions is SN
452pub fn coc_sn_ty() -> Expr {
453    prop()
454}
455/// PCFType: types of PCF (Plotkin's Programming Computable Functions)
456/// PCF = STLC + fixpoint + nat + bool
457pub fn pcf_type_ty() -> Expr {
458    type0()
459}
460/// PCFTerm: terms of PCF (including `fix`, `pred`, `succ`, `if-then-else`)
461pub fn pcf_term_ty() -> Expr {
462    type0()
463}
464/// PCFFixpoint: the fixed-point operator `fix : (τ → τ) → τ` in PCF
465pub fn pcf_fixpoint_ty() -> Expr {
466    pi(
467        BinderInfo::Default,
468        "tau",
469        simple_type_ty(),
470        arrow(arrow(bvar(0), bvar(1)), bvar(0)),
471    )
472}
473/// PCFTyping: typing judgment for PCF
474pub fn pcf_typing_ty() -> Expr {
475    arrow(
476        typing_context_ty(),
477        arrow(pcf_term_ty(), arrow(pcf_type_ty(), prop())),
478    )
479}
480/// PCFDenotationalSemantics: Scott domain semantics for PCF
481pub fn pcf_denotational_semantics_ty() -> Expr {
482    prop()
483}
484/// PCFAdequacy: operational and denotational semantics agree for PCF
485pub fn pcf_adequacy_ty() -> Expr {
486    prop()
487}
488/// PCFFullAbstraction: Milner's full abstraction problem for PCF
489pub fn pcf_full_abstraction_ty() -> Expr {
490    prop()
491}
492/// SubtypeRelation: A <: B (A is a subtype of B)
493pub fn subtype_relation_ty() -> Expr {
494    arrow(simple_type_ty(), arrow(simple_type_ty(), prop()))
495}
496/// SubtypingReflexivity: A <: A
497pub fn subtyping_reflexivity_ty() -> Expr {
498    arrow(simple_type_ty(), prop())
499}
500/// SubtypingTransitivity: A <: B → B <: C → A <: C
501pub fn subtyping_transitivity_ty() -> Expr {
502    arrow(
503        simple_type_ty(),
504        arrow(simple_type_ty(), arrow(simple_type_ty(), prop())),
505    )
506}
507/// BoundedQuantification: ∀ X <: T. U (F-sub style bounded ∀)
508pub fn bounded_quantification_ty() -> Expr {
509    arrow(
510        simple_type_ty(),
511        arrow(arrow(simple_type_ty(), simple_type_ty()), simple_type_ty()),
512    )
513}
514/// FBoundedPolymorphism: F-bounded quantification ∀ X <: F\[X\]. U
515pub fn f_bounded_polymorphism_ty() -> Expr {
516    arrow(
517        arrow(simple_type_ty(), simple_type_ty()),
518        arrow(arrow(simple_type_ty(), simple_type_ty()), simple_type_ty()),
519    )
520}
521/// CoercionFunction: a coercion c : A → B witnessing A <: B
522pub fn coercion_function_ty() -> Expr {
523    arrow(simple_type_ty(), arrow(simple_type_ty(), prop()))
524}
525/// SubtypingSubjectReduction: subtying is preserved under reduction
526pub fn subtyping_subject_reduction_ty() -> Expr {
527    prop()
528}
529/// EffectLabel: a label for a computational effect
530pub fn effect_label_ty() -> Expr {
531    type0()
532}
533/// EffectSet: a set of effect labels
534pub fn effect_set_ty() -> Expr {
535    type0()
536}
537/// EffectType: a type annotated with effects τ !ε
538pub fn effect_type_ty() -> Expr {
539    arrow(simple_type_ty(), arrow(effect_set_ty(), simple_type_ty()))
540}
541/// EffectTyping: Γ ⊢ t : τ ! ε
542pub fn effect_typing_ty() -> Expr {
543    arrow(
544        typing_context_ty(),
545        arrow(
546            untyped_term_ty(),
547            arrow(simple_type_ty(), arrow(effect_set_ty(), prop())),
548        ),
549    )
550}
551/// RegionType: a type annotated with memory region ρ
552pub fn region_type_ty() -> Expr {
553    type0()
554}
555/// RegionInference: algorithm to infer region annotations
556pub fn region_inference_ty() -> Expr {
557    arrow(untyped_term_ty(), region_type_ty())
558}
559/// GradedType: a type T graded by a semiring element r (coeffect)
560pub fn graded_type_ty() -> Expr {
561    type0()
562}
563/// CoeffectSystem: a type system tracking resource usage via graded types
564pub fn coeffect_system_ty() -> Expr {
565    type0()
566}
567/// CoeffectTyping: Γ ⊢ t : T graded by r
568pub fn coeffect_typing_ty() -> Expr {
569    arrow(
570        typing_context_ty(),
571        arrow(untyped_term_ty(), arrow(graded_type_ty(), prop())),
572    )
573}
574/// LinearType: a type that must be used exactly once
575pub fn linear_type_ty() -> Expr {
576    type0()
577}
578/// LinearContext: a linear typing context (each variable used exactly once)
579pub fn linear_context_ty() -> Expr {
580    type0()
581}
582/// LinearTyping: linear typing judgment Γ ⊢_L t : A
583pub fn linear_typing_ty() -> Expr {
584    arrow(
585        linear_context_ty(),
586        arrow(untyped_term_ty(), arrow(linear_type_ty(), prop())),
587    )
588}
589/// LinearArrow: the linear function type A ⊸ B
590pub fn linear_arrow_ty() -> Expr {
591    arrow(linear_type_ty(), arrow(linear_type_ty(), linear_type_ty()))
592}
593/// LinearExchangeability: linear contexts can be reordered
594pub fn linear_exchangeability_ty() -> Expr {
595    prop()
596}
597/// AffineType: a type that may be used at most once (weakening allowed)
598pub fn affine_type_ty() -> Expr {
599    type0()
600}
601/// AffineTyping: affine typing judgment (weakening OK, no contraction)
602pub fn affine_typing_ty() -> Expr {
603    arrow(
604        typing_context_ty(),
605        arrow(untyped_term_ty(), arrow(affine_type_ty(), prop())),
606    )
607}
608/// RelevantType: a type that must be used at least once (contraction OK, no weakening)
609pub fn relevant_type_ty() -> Expr {
610    type0()
611}
612/// RelevantTyping: relevant typing judgment
613pub fn relevant_typing_ty() -> Expr {
614    arrow(
615        typing_context_ty(),
616        arrow(untyped_term_ty(), arrow(relevant_type_ty(), prop())),
617    )
618}
619/// BangModality: the `!A` modality — unrestricted use of A
620pub fn bang_modality_ty() -> Expr {
621    arrow(linear_type_ty(), linear_type_ty())
622}
623/// LFSignature: a signature Σ in Edinburgh LF
624pub fn lf_signature_ty() -> Expr {
625    type0()
626}
627/// LFContext: a context Γ in Edinburgh LF
628pub fn lf_context_ty() -> Expr {
629    type0()
630}
631/// LFTyping: Σ; Γ ⊢ t : T in Edinburgh LF
632pub fn lf_typing_ty() -> Expr {
633    arrow(
634        lf_signature_ty(),
635        arrow(
636            lf_context_ty(),
637            arrow(untyped_term_ty(), arrow(untyped_term_ty(), prop())),
638        ),
639    )
640}
641/// LFKindValidity: Σ; Γ ⊢ K kind
642pub fn lf_kind_validity_ty() -> Expr {
643    arrow(
644        lf_signature_ty(),
645        arrow(lf_context_ty(), arrow(kind_ty(), prop())),
646    )
647}
648/// UTTUniverse: a universe in Luo's Unified Theory of Types
649pub fn utt_universe_ty() -> Expr {
650    type0()
651}
652/// UTTELType: a type in UTT (el-form, deriving a type from a set)
653pub fn utt_el_type_ty() -> Expr {
654    arrow(utt_universe_ty(), type0())
655}
656/// CICInductiveType: an inductive type in the Calculus of Inductive Constructions
657pub fn cic_inductive_type_ty() -> Expr {
658    type0()
659}
660/// CICElimination: the elimination/recursor for an inductive type
661pub fn cic_elimination_ty() -> Expr {
662    arrow(cic_inductive_type_ty(), untyped_term_ty())
663}
664/// CICPositivityCondition: strict positivity for inductive types
665pub fn cic_positivity_condition_ty() -> Expr {
666    arrow(cic_inductive_type_ty(), prop())
667}
668/// IntersectionType: A ∩ B — a term has both types A and B
669pub fn intersection_type_ty() -> Expr {
670    arrow(simple_type_ty(), arrow(simple_type_ty(), simple_type_ty()))
671}
672/// IntersectionTyping: Γ ⊢ t : A ∩ B
673pub fn intersection_typing_ty() -> Expr {
674    arrow(
675        typing_context_ty(),
676        arrow(untyped_term_ty(), arrow(simple_type_ty(), prop())),
677    )
678}
679/// FilterModel: a filter model of the untyped λ-calculus via intersection types
680pub fn filter_model_ty() -> Expr {
681    type0()
682}
683/// IntersectionTypeCompleteness: every normalizable term is typeable
684pub fn intersection_type_completeness_ty() -> Expr {
685    prop()
686}
687/// PrincipalTyping: every typeable term has a principal type scheme
688pub fn principal_typing_ty() -> Expr {
689    arrow(untyped_term_ty(), prop())
690}
691/// UnionType: A ∪ B — occurrence typing context
692pub fn union_type_ty() -> Expr {
693    arrow(simple_type_ty(), arrow(simple_type_ty(), simple_type_ty()))
694}
695/// OccurrenceTyping: type assignment based on control flow occurrences
696pub fn occurrence_typing_ty() -> Expr {
697    arrow(
698        typing_context_ty(),
699        arrow(untyped_term_ty(), arrow(simple_type_ty(), prop())),
700    )
701}
702/// FlowAnalysis: 0-CFA / control-flow analysis as a type system
703pub fn flow_analysis_ty() -> Expr {
704    arrow(untyped_term_ty(), type0())
705}
706/// GradualType: a type that may be partially unknown (includes `?`)
707pub fn gradual_type_ty() -> Expr {
708    type0()
709}
710/// DynType: the dynamic type `?` (unknown type)
711pub fn dyn_type_ty() -> Expr {
712    gradual_type_ty()
713}
714/// TypeConsistency: A ~ B (types are consistent, i.e., compatible under `?`)
715pub fn type_consistency_ty() -> Expr {
716    arrow(gradual_type_ty(), arrow(gradual_type_ty(), prop()))
717}
718/// GradualTyping: Γ ⊢ t : A in the gradually-typed λ-calculus
719pub fn gradual_typing_ty() -> Expr {
720    arrow(
721        typing_context_ty(),
722        arrow(untyped_term_ty(), arrow(gradual_type_ty(), prop())),
723    )
724}
725/// BlameLabel: a label tracking the source of a runtime type failure
726pub fn blame_label_ty() -> Expr {
727    type0()
728}
729/// BlameCalculusTerm: a term in the blame calculus (with casts and labels)
730pub fn blame_calculus_term_ty() -> Expr {
731    type0()
732}
733/// BlameTheorem: well-typed programs can only be blamed at boundaries
734pub fn blame_theorem_ty() -> Expr {
735    prop()
736}
737/// AbstractingGradualTyping: AGT framework lifting predicates to gradual types
738pub fn abstracting_gradual_typing_ty() -> Expr {
739    prop()
740}
741/// SessionType: the type of a communication channel endpoint
742pub fn session_type_ty() -> Expr {
743    type0()
744}
745/// SendType: !T.S — send a value of type T then continue as S
746pub fn send_type_ty() -> Expr {
747    arrow(
748        simple_type_ty(),
749        arrow(session_type_ty(), session_type_ty()),
750    )
751}
752/// RecvType: ?T.S — receive a value of type T then continue as S
753pub fn recv_type_ty() -> Expr {
754    arrow(
755        simple_type_ty(),
756        arrow(session_type_ty(), session_type_ty()),
757    )
758}
759/// EndType: the completed session
760pub fn end_type_ty() -> Expr {
761    session_type_ty()
762}
763/// DualSession: the dual of a session type (swap sends and receives)
764pub fn dual_session_ty() -> Expr {
765    arrow(session_type_ty(), session_type_ty())
766}
767/// BinarySessionTyping: Γ ⊢ P : S (binary session typing)
768pub fn binary_session_typing_ty() -> Expr {
769    arrow(
770        typing_context_ty(),
771        arrow(untyped_term_ty(), arrow(session_type_ty(), prop())),
772    )
773}
774/// MultipartySessionType: a global type for multiparty session protocols
775pub fn multiparty_session_type_ty() -> Expr {
776    type0()
777}
778/// GlobalToLocal: project a global type to a local session type for a role
779pub fn global_to_local_ty() -> Expr {
780    arrow(
781        multiparty_session_type_ty(),
782        arrow(nat_ty(), session_type_ty()),
783    )
784}
785/// DeadlockFreedom: well-typed session processes do not deadlock
786pub fn deadlock_freedom_ty() -> Expr {
787    prop()
788}
789/// SessionTypeCompleteness: every interaction satisfying the global type is typeable
790pub fn session_type_completeness_ty() -> Expr {
791    prop()
792}
793/// RecursiveType: a type μX.F\[X\] — least fixed point of type functor F
794pub fn recursive_type_ty() -> Expr {
795    arrow(arrow(simple_type_ty(), simple_type_ty()), simple_type_ty())
796}
797/// IsoRecursiveFold: fold : F\[μX.F\] → μX.F
798pub fn iso_recursive_fold_ty() -> Expr {
799    arrow(
800        arrow(simple_type_ty(), simple_type_ty()),
801        arrow(simple_type_ty(), simple_type_ty()),
802    )
803}
804/// IsoRecursiveUnfold: unfold : μX.F → F\[μX.F\]
805pub fn iso_recursive_unfold_ty() -> Expr {
806    arrow(
807        arrow(simple_type_ty(), simple_type_ty()),
808        arrow(simple_type_ty(), simple_type_ty()),
809    )
810}
811/// EquiRecursiveType: equi-recursive interpretation (fold/unfold invisible)
812pub fn equi_recursive_type_ty() -> Expr {
813    arrow(arrow(simple_type_ty(), simple_type_ty()), simple_type_ty())
814}
815/// TypeUnrolling: μX.F ≡ F\[μX.F\] (equi-recursive unrolling)
816pub fn type_unrolling_ty() -> Expr {
817    arrow(arrow(simple_type_ty(), simple_type_ty()), prop())
818}
819/// RecursiveTypeContraction: well-founded recursive types have unique fixed points
820pub fn recursive_type_contraction_ty() -> Expr {
821    prop()
822}
823/// KindPolymorphism: ∀κ. F\[κ\] — quantification over kinds
824pub fn kind_polymorphism_ty() -> Expr {
825    arrow(arrow(kind_ty(), kind_ty()), kind_ty())
826}
827/// HigherKindedType: a type constructor of kind κ ⇒ κ'
828pub fn higher_kinded_type_ty() -> Expr {
829    arrow(kind_ty(), arrow(kind_ty(), type0()))
830}
831/// KindInference: algorithm to infer kinds for type expressions
832pub fn kind_inference_ty() -> Expr {
833    arrow(system_fomega_type_ty(), option_ty(kind_ty()))
834}
835/// KindSoundness: well-kinded type applications have well-kinded results
836pub fn kind_soundness_ty() -> Expr {
837    prop()
838}
839/// KindCompleteness: kind inference is complete for Fω types
840pub fn kind_completeness_ty() -> Expr {
841    prop()
842}
843/// RowType: a row of labeled types (for records or variants)
844pub fn row_type_ty() -> Expr {
845    type0()
846}
847/// ExtendRow: add a field l : T to a row R
848pub fn extend_row_ty() -> Expr {
849    arrow(
850        nat_ty(),
851        arrow(simple_type_ty(), arrow(row_type_ty(), row_type_ty())),
852    )
853}
854/// EmptyRow: the empty row
855pub fn empty_row_ty() -> Expr {
856    row_type_ty()
857}
858/// RecordType: a closed record type from a row
859pub fn record_type_ty() -> Expr {
860    arrow(row_type_ty(), simple_type_ty())
861}
862/// VariantType: a closed variant type from a row
863pub fn variant_type_ty() -> Expr {
864    arrow(row_type_ty(), simple_type_ty())
865}
866/// RowPolymorphicTyping: Γ ⊢ t : {R} with row variable R
867pub fn row_polymorphic_typing_ty() -> Expr {
868    arrow(
869        typing_context_ty(),
870        arrow(untyped_term_ty(), arrow(row_type_ty(), prop())),
871    )
872}
873/// StructuralSubtyping: subtyping determined by structure, not names
874pub fn structural_subtyping_ty() -> Expr {
875    arrow(row_type_ty(), arrow(row_type_ty(), prop()))
876}
877/// SetoidCarrier: the carrier set of a setoid
878pub fn setoid_carrier_ty() -> Expr {
879    type0()
880}
881/// SetoidRelation: the equivalence relation of a setoid
882pub fn setoid_relation_ty() -> Expr {
883    arrow(setoid_carrier_ty(), arrow(setoid_carrier_ty(), prop()))
884}
885/// Setoid: a pair of a carrier and an equivalence relation
886pub fn setoid_ty() -> Expr {
887    type0()
888}
889/// QuotientType: the quotient A / ~ of a setoid
890pub fn quotient_type_ty() -> Expr {
891    arrow(setoid_ty(), type0())
892}
893/// QuotientIntro: \[a\] : A / ~ (introduction rule)
894pub fn quotient_intro_ty() -> Expr {
895    arrow(setoid_ty(), arrow(setoid_carrier_ty(), quotient_type_ty()))
896}
897/// QuotientElim: elimination from A / ~ to a P that respects ~
898pub fn quotient_elim_ty() -> Expr {
899    arrow(
900        setoid_ty(),
901        arrow(
902            arrow(setoid_carrier_ty(), type0()),
903            arrow(quotient_type_ty(), type0()),
904        ),
905    )
906}
907/// QuotientComputation: \[a\] elim f = f a
908pub fn quotient_computation_ty() -> Expr {
909    arrow(setoid_ty(), prop())
910}
911/// ProofIrrelevance: any two proofs of the same proposition are equal
912pub fn proof_irrelevance_ty() -> Expr {
913    pi(
914        BinderInfo::Default,
915        "P",
916        prop(),
917        pi(
918            BinderInfo::Default,
919            "p",
920            bvar(0),
921            pi(BinderInfo::Default, "q", bvar(1), prop()),
922        ),
923    )
924}
925/// IrrelevantArgument: a term whose type-theoretic argument is proof-irrelevant
926pub fn irrelevant_argument_ty() -> Expr {
927    arrow(prop(), prop())
928}
929/// SquashType: propositional truncation ||A|| (collapse all proofs)
930pub fn squash_type_ty() -> Expr {
931    arrow(type0(), prop())
932}
933/// SquashIntro: a : A → ||A||
934pub fn squash_intro_ty() -> Expr {
935    arrow(type0(), arrow(type0(), prop()))
936}
937/// SquashElim: ||A|| → (A → P) → P for P : Prop
938pub fn squash_elim_ty() -> Expr {
939    arrow(prop(), arrow(arrow(type0(), prop()), prop()))
940}
941/// UniverseLevel: the type of universe levels (ω-many levels)
942pub fn universe_level_ty() -> Expr {
943    nat_ty()
944}
945/// RussellUniverse: Uᵢ : Uᵢ₊₁ in the Russell style (types live in universes)
946pub fn russell_universe_ty() -> Expr {
947    arrow(universe_level_ty(), type1())
948}
949/// TarskiUniverse: a Tarski-style universe Uᵢ with a decoding map elᵢ
950pub fn tarski_universe_ty() -> Expr {
951    type0()
952}
953/// TarskiDecode: el : Uᵢ → Type (decode a code to a type)
954pub fn tarski_decode_ty() -> Expr {
955    arrow(tarski_universe_ty(), type0())
956}
957/// CumulativeHierarchy: Uᵢ ⊆ Uᵢ₊₁ (lifting from one universe to the next)
958pub fn cumulative_hierarchy_ty() -> Expr {
959    arrow(
960        universe_level_ty(),
961        arrow(tarski_universe_ty(), tarski_universe_ty()),
962    )
963}
964/// UniversePolymorphism: quantification over universe levels
965pub fn universe_polymorphism_ty() -> Expr {
966    arrow(arrow(universe_level_ty(), type1()), type1())
967}
968/// ResizingAxiom: propositional resizing (all propositions are small)
969pub fn resizing_axiom_ty() -> Expr {
970    prop()
971}
972/// DelimitedContinuation: type of delimited continuation operators (shift/reset)
973pub fn delimited_continuation_ty() -> Expr {
974    arrow(simple_type_ty(), arrow(simple_type_ty(), simple_type_ty()))
975}
976/// MonadicType: a monadic type T M (T wrapped in monad M)
977pub fn monadic_type_ty() -> Expr {
978    arrow(
979        arrow(simple_type_ty(), simple_type_ty()),
980        arrow(simple_type_ty(), simple_type_ty()),
981    )
982}
983/// MonadicTyping: Γ ⊢ t : M\[A\] for monad M
984pub fn monadic_typing_ty() -> Expr {
985    arrow(
986        typing_context_ty(),
987        arrow(
988            untyped_term_ty(),
989            arrow(
990                arrow(simple_type_ty(), simple_type_ty()),
991                arrow(simple_type_ty(), prop()),
992            ),
993        ),
994    )
995}
996/// AlgebraicEffectType: a type for algebraic effects with operations Op
997pub fn algebraic_effect_type_ty() -> Expr {
998    type0()
999}
1000/// HandlerType: a handler mapping effects to values of type A
1001pub fn handler_type_ty() -> Expr {
1002    arrow(
1003        algebraic_effect_type_ty(),
1004        arrow(simple_type_ty(), simple_type_ty()),
1005    )
1006}
1007/// DependentSessionType: a session type indexed by values (dependent sessions)
1008pub fn dependent_session_type_ty() -> Expr {
1009    type0()
1010}
1011/// RefinementType: {x : T | P x} — a type refined by predicate P
1012pub fn refinement_type_ty() -> Expr {
1013    arrow(
1014        simple_type_ty(),
1015        arrow(arrow(simple_type_ty(), prop()), simple_type_ty()),
1016    )
1017}
1018/// LiquidType: refinement type with decidable predicates (Liquid Haskell style)
1019pub fn liquid_type_ty() -> Expr {
1020    arrow(
1021        simple_type_ty(),
1022        arrow(arrow(simple_type_ty(), bool_ty()), simple_type_ty()),
1023    )
1024}
1025/// NominalType: a type with freshness/name-binding (nominal logic)
1026pub fn nominal_type_ty() -> Expr {
1027    type0()
1028}
1029/// FreshnessPredicate: `a # t` — name a is fresh in term t
1030pub fn freshness_predicate_ty() -> Expr {
1031    arrow(nat_ty(), arrow(untyped_term_ty(), prop()))
1032}
1033/// AbstractionNominal: `⟨a⟩t` — nominal abstraction over fresh name a
1034pub fn abstraction_nominal_ty() -> Expr {
1035    arrow(nat_ty(), arrow(untyped_term_ty(), nominal_type_ty()))
1036}
1037/// Populate an `Environment` with lambda-calculus axioms and theorem stubs.
1038pub fn build_lambda_calculus_env() -> Environment {
1039    let mut env = Environment::new();
1040    let axioms: &[(&str, Expr)] = &[
1041        ("UntypedTerm", untyped_term_ty()),
1042        ("LcVariable", variable_ty()),
1043        ("LcAbstraction", abstraction_ty()),
1044        ("LcApplication", application_ty()),
1045        ("LcSubstitution", substitution_ty()),
1046        ("BetaRedex", beta_redex_ty()),
1047        ("EtaRedex", eta_redex_ty()),
1048        ("BetaStep", beta_step_ty()),
1049        ("EtaStep", eta_step_ty()),
1050        ("BetaReduction", beta_reduction_ty()),
1051        ("BetaEquiv", beta_equiv_ty()),
1052        ("NormalForm", normal_form_ty()),
1053        ("WeakNormalForm", weak_normal_form_ty()),
1054        ("HeadNormalForm", head_normal_form_ty()),
1055        ("ChurchNumeral", church_numeral_ty()),
1056        ("ChurchSucc", church_succ_ty()),
1057        ("ChurchPlus", church_plus_ty()),
1058        ("ChurchMul", church_mul_ty()),
1059        ("ChurchExp", church_exp_ty()),
1060        ("ChurchPred", church_pred_ty()),
1061        ("ChurchIsZero", church_is_zero_ty()),
1062        ("ChurchNumeralCorrect", church_numeral_correct_ty()),
1063        ("ChurchArithCorrect", church_arith_correct_ty()),
1064        ("YCombinator", y_combinator_ty()),
1065        ("TuringCombinator", turing_combinator_ty()),
1066        ("RecursionTheorem", recursion_theorem_ty()),
1067        ("YFixedPoint", y_fixed_point_ty()),
1068        ("OmegaCombinator", omega_combinator_ty()),
1069        ("OmegaDiverges", omega_diverges_ty()),
1070        ("NormalOrderRedex", normal_order_redex_ty()),
1071        ("ApplicativeOrderRedex", applicative_order_redex_ty()),
1072        ("HeadReduction", head_reduction_ty()),
1073        ("NormalOrderStrategy", normal_order_strategy_ty()),
1074        ("StandardizationTheorem", standardization_theorem_ty()),
1075        ("CallByValueReduction", cbv_reduction_ty()),
1076        ("CallByNeedReduction", cbn_reduction_ty()),
1077        ("DiamondProperty", diamond_property_ty()),
1078        ("ChurchRosserTheorem", church_rosser_theorem_ty()),
1079        ("Confluence", confluence_ty()),
1080        ("ParallelReduction", parallel_reduction_ty()),
1081        (
1082            "ParallelReductionComplete",
1083            parallel_reduction_complete_ty(),
1084        ),
1085        ("ParallelMaxReduct", parallel_max_reduct_ty()),
1086        (
1087            "ParallelMaxReductProperty",
1088            parallel_max_reduct_property_ty(),
1089        ),
1090        ("BohmTree", bohm_tree_ty()),
1091        ("BohmTreeOf", bohm_tree_of_ty()),
1092        ("UnsolvableTerm", unsolvable_term_ty()),
1093        ("SolvableTerm", solvable_term_ty()),
1094        ("BohmEquiv", bohm_equiv_ty()),
1095        ("ObservationalEquiv", observational_equiv_ty()),
1096        ("BohmTheorem", bohm_theorem_ty()),
1097        ("SimpleType", simple_type_ty()),
1098        ("BaseType", base_type_ty()),
1099        ("ArrowType", arrow_type_ty()),
1100        ("TypingContext", typing_context_ty()),
1101        ("STLCTyping", stlc_typing_ty()),
1102        ("STLCSubjectReduction", stlc_subject_reduction_ty()),
1103        ("STLCStrongNormalization", stlc_strong_normalization_ty()),
1104        ("STLCChurchRosser", stlc_church_rosser_ty()),
1105        ("STLCDecidability", stlc_decidability_ty()),
1106        ("SystemFType", system_f_type_ty()),
1107        ("SystemFTerm", system_f_term_ty()),
1108        ("SystemFTyping", system_f_typing_ty()),
1109        ("SystemFStrongNormalization", system_f_sn_ty()),
1110        ("SystemFConfluence", system_f_confluence_ty()),
1111        ("SystemFParametricity", system_f_parametricity_ty()),
1112        ("SystemFUndecidableTyping", system_f_undecidable_ty()),
1113        ("ChurchNatF", church_nat_f_ty()),
1114        ("ChurchBoolF", church_bool_f_ty()),
1115        ("ChurchListF", church_list_f_ty()),
1116        ("Kind", kind_ty()),
1117        ("StarKind", star_kind_ty()),
1118        ("KindArrow", kind_arrow_ty()),
1119        ("TypeConstructor", type_constructor_ty()),
1120        ("SystemFOmegaType", system_fomega_type_ty()),
1121        ("SystemFOmegaTerm", system_fomega_term_ty()),
1122        ("SystemFOmegaTyping", system_fomega_typing_ty()),
1123        ("SystemFOmegaSN", system_fomega_sn_ty()),
1124        (
1125            "SystemFOmegaKindSoundness",
1126            system_fomega_kind_soundness_ty(),
1127        ),
1128        ("PTSAxiom", pts_axiom_ty()),
1129        ("PTSRule", pts_rule_ty()),
1130        ("PureTypeSystem", pure_type_system_ty()),
1131        ("PTSTyping", pts_typing_ty()),
1132        ("CoC", coc_ty()),
1133        ("LambdaArrow", lambda_arrow_ty()),
1134        ("Lambda2", lambda2_ty()),
1135        ("LambdaOmega", lambda_omega_ty()),
1136        ("LambdaP", lambda_p_ty()),
1137        ("PTSSubjectReduction", pts_subject_reduction_ty()),
1138        ("PTSConfluence", pts_confluence_ty()),
1139        ("CoCStrongNormalization", coc_sn_ty()),
1140        ("PCFType", pcf_type_ty()),
1141        ("PCFTerm", pcf_term_ty()),
1142        ("PCFFixpoint", pcf_fixpoint_ty()),
1143        ("PCFTyping", pcf_typing_ty()),
1144        ("PCFDenotationalSemantics", pcf_denotational_semantics_ty()),
1145        ("PCFAdequacy", pcf_adequacy_ty()),
1146        ("PCFFullAbstraction", pcf_full_abstraction_ty()),
1147        ("SubtypeRelation", subtype_relation_ty()),
1148        ("SubtypingReflexivity", subtyping_reflexivity_ty()),
1149        ("SubtypingTransitivity", subtyping_transitivity_ty()),
1150        ("BoundedQuantification", bounded_quantification_ty()),
1151        ("FBoundedPolymorphism", f_bounded_polymorphism_ty()),
1152        ("CoercionFunction", coercion_function_ty()),
1153        (
1154            "SubtypingSubjectReduction",
1155            subtyping_subject_reduction_ty(),
1156        ),
1157        ("EffectLabel", effect_label_ty()),
1158        ("EffectSet", effect_set_ty()),
1159        ("EffectType", effect_type_ty()),
1160        ("EffectTyping", effect_typing_ty()),
1161        ("RegionType", region_type_ty()),
1162        ("RegionInference", region_inference_ty()),
1163        ("GradedType", graded_type_ty()),
1164        ("CoeffectSystem", coeffect_system_ty()),
1165        ("CoeffectTyping", coeffect_typing_ty()),
1166        ("LinearType", linear_type_ty()),
1167        ("LinearContext", linear_context_ty()),
1168        ("LinearTyping", linear_typing_ty()),
1169        ("LinearArrow", linear_arrow_ty()),
1170        ("LinearExchangeability", linear_exchangeability_ty()),
1171        ("AffineType", affine_type_ty()),
1172        ("AffineTyping", affine_typing_ty()),
1173        ("RelevantType", relevant_type_ty()),
1174        ("RelevantTyping", relevant_typing_ty()),
1175        ("BangModality", bang_modality_ty()),
1176        ("LFSignature", lf_signature_ty()),
1177        ("LFContext", lf_context_ty()),
1178        ("LFTyping", lf_typing_ty()),
1179        ("LFKindValidity", lf_kind_validity_ty()),
1180        ("UTTUniverse", utt_universe_ty()),
1181        ("UTTELType", utt_el_type_ty()),
1182        ("CICInductiveType", cic_inductive_type_ty()),
1183        ("CICElimination", cic_elimination_ty()),
1184        ("CICPositivityCondition", cic_positivity_condition_ty()),
1185        ("IntersectionType", intersection_type_ty()),
1186        ("IntersectionTyping", intersection_typing_ty()),
1187        ("FilterModel", filter_model_ty()),
1188        (
1189            "IntersectionTypeCompleteness",
1190            intersection_type_completeness_ty(),
1191        ),
1192        ("PrincipalTyping", principal_typing_ty()),
1193        ("UnionType", union_type_ty()),
1194        ("OccurrenceTyping", occurrence_typing_ty()),
1195        ("FlowAnalysis", flow_analysis_ty()),
1196        ("GradualType", gradual_type_ty()),
1197        ("DynType", dyn_type_ty()),
1198        ("TypeConsistency", type_consistency_ty()),
1199        ("GradualTyping", gradual_typing_ty()),
1200        ("BlameLabel", blame_label_ty()),
1201        ("BlameCalculusTerm", blame_calculus_term_ty()),
1202        ("BlameTheorem", blame_theorem_ty()),
1203        ("AbstractingGradualTyping", abstracting_gradual_typing_ty()),
1204        ("SessionType", session_type_ty()),
1205        ("SendType", send_type_ty()),
1206        ("RecvType", recv_type_ty()),
1207        ("EndType", end_type_ty()),
1208        ("DualSession", dual_session_ty()),
1209        ("BinarySessionTyping", binary_session_typing_ty()),
1210        ("MultipartySessionType", multiparty_session_type_ty()),
1211        ("GlobalToLocal", global_to_local_ty()),
1212        ("DeadlockFreedom", deadlock_freedom_ty()),
1213        ("SessionTypeCompleteness", session_type_completeness_ty()),
1214        ("RecursiveType", recursive_type_ty()),
1215        ("IsoRecursiveFold", iso_recursive_fold_ty()),
1216        ("IsoRecursiveUnfold", iso_recursive_unfold_ty()),
1217        ("EquiRecursiveType", equi_recursive_type_ty()),
1218        ("TypeUnrolling", type_unrolling_ty()),
1219        ("RecursiveTypeContraction", recursive_type_contraction_ty()),
1220        ("KindPolymorphism", kind_polymorphism_ty()),
1221        ("HigherKindedType", higher_kinded_type_ty()),
1222        ("KindInference", kind_inference_ty()),
1223        ("KindSoundness", kind_soundness_ty()),
1224        ("KindCompleteness", kind_completeness_ty()),
1225        ("RowType", row_type_ty()),
1226        ("ExtendRow", extend_row_ty()),
1227        ("EmptyRow", empty_row_ty()),
1228        ("RecordType", record_type_ty()),
1229        ("VariantType", variant_type_ty()),
1230        ("RowPolymorphicTyping", row_polymorphic_typing_ty()),
1231        ("StructuralSubtyping", structural_subtyping_ty()),
1232        ("SetoidCarrier", setoid_carrier_ty()),
1233        ("SetoidRelation", setoid_relation_ty()),
1234        ("Setoid", setoid_ty()),
1235        ("QuotientType", quotient_type_ty()),
1236        ("QuotientIntro", quotient_intro_ty()),
1237        ("QuotientElim", quotient_elim_ty()),
1238        ("QuotientComputation", quotient_computation_ty()),
1239        ("ProofIrrelevance", proof_irrelevance_ty()),
1240        ("IrrelevantArgument", irrelevant_argument_ty()),
1241        ("SquashType", squash_type_ty()),
1242        ("SquashIntro", squash_intro_ty()),
1243        ("SquashElim", squash_elim_ty()),
1244        ("UniverseLevel", universe_level_ty()),
1245        ("RussellUniverse", russell_universe_ty()),
1246        ("TarskiUniverse", tarski_universe_ty()),
1247        ("TarskiDecode", tarski_decode_ty()),
1248        ("CumulativeHierarchy", cumulative_hierarchy_ty()),
1249        ("UniversePolymorphism", universe_polymorphism_ty()),
1250        ("ResizingAxiom", resizing_axiom_ty()),
1251        ("DelimitedContinuation", delimited_continuation_ty()),
1252        ("MonadicType", monadic_type_ty()),
1253        ("MonadicTyping", monadic_typing_ty()),
1254        ("AlgebraicEffectType", algebraic_effect_type_ty()),
1255        ("HandlerType", handler_type_ty()),
1256        ("DependentSessionType", dependent_session_type_ty()),
1257        ("RefinementType", refinement_type_ty()),
1258        ("LiquidType", liquid_type_ty()),
1259        ("NominalType", nominal_type_ty()),
1260        ("FreshnessPredicate", freshness_predicate_ty()),
1261        ("AbstractionNominal", abstraction_nominal_ty()),
1262    ];
1263    for (name, ty) in axioms {
1264        env.add(Declaration::Axiom {
1265            name: Name::str(*name),
1266            univ_params: vec![],
1267            ty: ty.clone(),
1268        })
1269        .ok();
1270    }
1271    env
1272}
1273/// Build the Church numeral for `n`.
1274/// c_n = λf. λx. f^n x
1275pub fn church(n: usize) -> Term {
1276    let x = Term::Var(0);
1277    let f = Term::Var(1);
1278    let mut body = x;
1279    for _ in 0..n {
1280        body = Term::App(Box::new(f.clone()), Box::new(body));
1281    }
1282    Term::Lam(Box::new(Term::Lam(Box::new(body))))
1283}
1284/// Church successor: S = λn. λf. λx. f (n f x)
1285pub fn church_succ() -> Term {
1286    let n = Term::Var(2);
1287    let f = Term::Var(1);
1288    let x = Term::Var(0);
1289    let nfx = Term::App(
1290        Box::new(Term::App(Box::new(n), Box::new(f.clone()))),
1291        Box::new(x),
1292    );
1293    let body = Term::App(Box::new(f), Box::new(nfx));
1294    Term::Lam(Box::new(Term::Lam(Box::new(Term::Lam(Box::new(body))))))
1295}
1296/// Church addition: PLUS = λm. λn. λf. λx. m f (n f x)
1297pub fn church_plus() -> Term {
1298    let m = Term::Var(3);
1299    let n = Term::Var(2);
1300    let f = Term::Var(1);
1301    let x = Term::Var(0);
1302    let nfx = Term::App(
1303        Box::new(Term::App(Box::new(n), Box::new(f.clone()))),
1304        Box::new(x),
1305    );
1306    let body = Term::App(Box::new(Term::App(Box::new(m), Box::new(f))), Box::new(nfx));
1307    Term::Lam(Box::new(Term::Lam(Box::new(Term::Lam(Box::new(
1308        Term::Lam(Box::new(body)),
1309    ))))))
1310}
1311/// Church multiplication: MUL = λm. λn. λf. m (n f)
1312pub fn church_mul() -> Term {
1313    let m = Term::Var(2);
1314    let n = Term::Var(1);
1315    let f = Term::Var(0);
1316    let nf = Term::App(Box::new(n), Box::new(f));
1317    let body = Term::App(Box::new(m), Box::new(nf));
1318    Term::Lam(Box::new(Term::Lam(Box::new(Term::Lam(Box::new(body))))))
1319}
1320/// Apply PLUS to two Church numerals and reduce to normal form.
1321pub fn church_add(m: usize, n: usize) -> Term {
1322    let plus = church_plus();
1323    let cm = church(m);
1324    let cn = church(n);
1325    let applied = Term::App(
1326        Box::new(Term::App(Box::new(plus), Box::new(cm))),
1327        Box::new(cn),
1328    );
1329    let (result, _) = applied.normalize(10000);
1330    result
1331}
1332/// Type inference for the simply-typed lambda calculus (Curry style).
1333/// Returns `Some(ty)` if the term is typeable, `None` otherwise.
1334pub fn infer_type(ctx: &Context, term: &Term) -> Option<SimpleType> {
1335    match term {
1336        Term::Var(k) => ctx.get(*k).cloned(),
1337        Term::Lam(body) => {
1338            let _ = body;
1339            None
1340        }
1341        Term::App(f, a) => match infer_type(ctx, f)? {
1342            SimpleType::Arrow(dom, cod) => {
1343                if check_type(ctx, a, &dom) {
1344                    Some(*cod)
1345                } else {
1346                    None
1347                }
1348            }
1349            _ => None,
1350        },
1351    }
1352}
1353/// Type checking for the simply-typed lambda calculus.
1354/// Returns `true` iff `ctx ⊢ term : ty`.
1355pub fn check_type(ctx: &Context, term: &Term, ty: &SimpleType) -> bool {
1356    match (term, ty) {
1357        (Term::Lam(body), SimpleType::Arrow(dom, cod)) => {
1358            let ctx2 = ctx.extend(*dom.clone());
1359            check_type(&ctx2, body, cod)
1360        }
1361        (Term::App(f, a), _) => {
1362            if let Some(ft) = infer_type(ctx, f) {
1363                match ft {
1364                    SimpleType::Arrow(dom, cod) => *cod == *ty && check_type(ctx, a, &dom),
1365                    _ => false,
1366                }
1367            } else {
1368                false
1369            }
1370        }
1371        (Term::Var(k), _) => ctx.get(*k).map(|t| t == ty).unwrap_or(false),
1372        _ => false,
1373    }
1374}
1375/// Perform one-step β-reduction under the given strategy.
1376pub fn beta_step(term: &Term, strategy: Strategy) -> Option<Term> {
1377    match strategy {
1378        Strategy::NormalOrder => term.beta_step_normal(),
1379        Strategy::ApplicativeOrder => beta_step_applicative(term),
1380        Strategy::HeadReduction => beta_step_head(term),
1381    }
1382}
1383pub fn beta_step_applicative(term: &Term) -> Option<Term> {
1384    match term {
1385        Term::App(f, a) => {
1386            if let Some(a2) = beta_step_applicative(a) {
1387                return Some(Term::App(f.clone(), Box::new(a2)));
1388            }
1389            if let Some(f2) = beta_step_applicative(f) {
1390                return Some(Term::App(Box::new(f2), a.clone()));
1391            }
1392            if let Term::Lam(body) = f.as_ref() {
1393                return Some(body.subst(0, a));
1394            }
1395            None
1396        }
1397        Term::Lam(body) => beta_step_applicative(body).map(|b2| Term::Lam(Box::new(b2))),
1398        Term::Var(_) => None,
1399    }
1400}
1401pub fn beta_step_head(term: &Term) -> Option<Term> {
1402    match term {
1403        Term::App(f, a) => {
1404            if let Term::Lam(body) = f.as_ref() {
1405                return Some(body.subst(0, a));
1406            }
1407            beta_step_head(f).map(|f2| Term::App(Box::new(f2), a.clone()))
1408        }
1409        Term::Lam(body) => beta_step_head(body).map(|b2| Term::Lam(Box::new(b2))),
1410        Term::Var(_) => None,
1411    }
1412}
1413/// Result of linearity checking: a map from de Bruijn level → usage count.
1414#[allow(dead_code)]
1415pub type UsageMap = Vec<usize>;
1416#[cfg(test)]
1417mod tests {
1418    use super::*;
1419    /// Verify that the environment builds and contains key axioms.
1420    #[test]
1421    fn test_build_lambda_calculus_env() {
1422        let env = build_lambda_calculus_env();
1423        assert!(env.get(&Name::str("UntypedTerm")).is_some());
1424        assert!(env.get(&Name::str("YCombinator")).is_some());
1425        assert!(env.get(&Name::str("ChurchRosserTheorem")).is_some());
1426        assert!(env.get(&Name::str("SystemFStrongNormalization")).is_some());
1427        assert!(env.get(&Name::str("CoC")).is_some());
1428        assert!(env.get(&Name::str("BohmTheorem")).is_some());
1429    }
1430    /// Test Church numeral construction and normalization.
1431    #[test]
1432    fn test_church_numerals() {
1433        let c0 = church(0);
1434        assert_eq!(c0, Term::Lam(Box::new(Term::Lam(Box::new(Term::Var(0))))));
1435        let c1 = church(1);
1436        assert_eq!(
1437            c1,
1438            Term::Lam(Box::new(Term::Lam(Box::new(Term::App(
1439                Box::new(Term::Var(1)),
1440                Box::new(Term::Var(0))
1441            )))))
1442        );
1443        let c2 = church(2);
1444        assert!(c2.is_normal());
1445    }
1446    /// Test Church addition: 2 + 3 = 5.
1447    #[test]
1448    fn test_church_addition() {
1449        let result = church_add(2, 3);
1450        let expected = church(5);
1451        let (rn, _) = result.normalize(10000);
1452        let (en, _) = expected.normalize(10000);
1453        assert_eq!(rn, en);
1454    }
1455    /// Test beta-reduction: (λx.x) t →β t.
1456    #[test]
1457    fn test_identity_reduction() {
1458        let id = Term::Lam(Box::new(Term::Var(0)));
1459        let arg = Term::Var(0);
1460        let redex = Term::App(Box::new(id), Box::new(arg.clone()));
1461        let (result, steps) = redex.normalize(100);
1462        assert!(steps > 0);
1463        assert!(result.is_normal());
1464    }
1465    /// Test is_normal: variable and abstraction of variable are normal.
1466    #[test]
1467    fn test_is_normal() {
1468        assert!(Term::Var(0).is_normal());
1469        assert!(Term::Lam(Box::new(Term::Var(0))).is_normal());
1470        let redex = Term::App(
1471            Box::new(Term::Lam(Box::new(Term::Var(0)))),
1472            Box::new(Term::Var(1)),
1473        );
1474        assert!(!redex.is_normal());
1475    }
1476    /// Test type checking: identity function I : (α → α).
1477    #[test]
1478    fn test_stlc_identity() {
1479        let alpha = SimpleType::Base("α".into());
1480        let id = Term::Lam(Box::new(Term::Var(0)));
1481        let arrow_ty = SimpleType::arr(alpha.clone(), alpha.clone());
1482        let ctx = Context::empty();
1483        assert!(check_type(&ctx, &id, &arrow_ty));
1484    }
1485    /// Test type checking: K combinator K : α → β → α.
1486    #[test]
1487    fn test_stlc_k_combinator() {
1488        let alpha = SimpleType::Base("α".into());
1489        let beta = SimpleType::Base("β".into());
1490        let k = Term::Lam(Box::new(Term::Lam(Box::new(Term::Var(1)))));
1491        let ty = SimpleType::arr(alpha.clone(), SimpleType::arr(beta.clone(), alpha.clone()));
1492        let ctx = Context::empty();
1493        assert!(check_type(&ctx, &k, &ty));
1494    }
1495    /// Test reduction strategies: normal order vs. applicative order.
1496    #[test]
1497    fn test_reduction_strategies() {
1498        let id = || Term::Lam(Box::new(Term::Var(0)));
1499        let t = Term::App(
1500            Box::new(id()),
1501            Box::new(Term::App(Box::new(id()), Box::new(Term::Var(1)))),
1502        );
1503        assert!(!t.is_normal());
1504        let step_no = beta_step(&t, Strategy::NormalOrder);
1505        assert!(step_no.is_some());
1506        let step_ao = beta_step(&t, Strategy::ApplicativeOrder);
1507        assert!(step_ao.is_some());
1508    }
1509    /// Test that church(n) has correct size (2n+3 nodes).
1510    #[test]
1511    fn test_church_size() {
1512        assert_eq!(church(0).size(), 3);
1513        assert_eq!(church(1).size(), 5);
1514        let c3 = church(3);
1515        assert_eq!(c3.size(), 2 * 3 + 3);
1516    }
1517    /// Verify new axioms are registered in the environment.
1518    #[test]
1519    fn test_new_axioms_registered() {
1520        let env = build_lambda_calculus_env();
1521        assert!(env.get(&Name::str("PCFFixpoint")).is_some());
1522        assert!(env.get(&Name::str("PCFAdequacy")).is_some());
1523        assert!(env.get(&Name::str("BoundedQuantification")).is_some());
1524        assert!(env.get(&Name::str("FBoundedPolymorphism")).is_some());
1525        assert!(env.get(&Name::str("CoeffectSystem")).is_some());
1526        assert!(env.get(&Name::str("RegionInference")).is_some());
1527        assert!(env.get(&Name::str("LinearTyping")).is_some());
1528        assert!(env.get(&Name::str("BangModality")).is_some());
1529        assert!(env.get(&Name::str("AffineTyping")).is_some());
1530        assert!(env.get(&Name::str("LFTyping")).is_some());
1531        assert!(env.get(&Name::str("CICInductiveType")).is_some());
1532        assert!(env.get(&Name::str("FilterModel")).is_some());
1533        assert!(env.get(&Name::str("PrincipalTyping")).is_some());
1534        assert!(env.get(&Name::str("FlowAnalysis")).is_some());
1535        assert!(env.get(&Name::str("TypeConsistency")).is_some());
1536        assert!(env.get(&Name::str("BlameTheorem")).is_some());
1537        assert!(env.get(&Name::str("DualSession")).is_some());
1538        assert!(env.get(&Name::str("DeadlockFreedom")).is_some());
1539        assert!(env.get(&Name::str("MultipartySessionType")).is_some());
1540        assert!(env.get(&Name::str("IsoRecursiveFold")).is_some());
1541        assert!(env.get(&Name::str("TypeUnrolling")).is_some());
1542        assert!(env.get(&Name::str("KindPolymorphism")).is_some());
1543        assert!(env.get(&Name::str("HigherKindedType")).is_some());
1544        assert!(env.get(&Name::str("RecordType")).is_some());
1545        assert!(env.get(&Name::str("StructuralSubtyping")).is_some());
1546        assert!(env.get(&Name::str("QuotientType")).is_some());
1547        assert!(env.get(&Name::str("QuotientElim")).is_some());
1548        assert!(env.get(&Name::str("ProofIrrelevance")).is_some());
1549        assert!(env.get(&Name::str("SquashType")).is_some());
1550        assert!(env.get(&Name::str("RussellUniverse")).is_some());
1551        assert!(env.get(&Name::str("CumulativeHierarchy")).is_some());
1552        assert!(env.get(&Name::str("RefinementType")).is_some());
1553        assert!(env.get(&Name::str("NominalType")).is_some());
1554        assert!(env.get(&Name::str("AlgebraicEffectType")).is_some());
1555    }
1556    #[test]
1557    fn test_beta_reducer_converges() {
1558        let reducer = BetaReducer::new(Strategy::NormalOrder, 1000);
1559        let id = Term::Lam(Box::new(Term::Var(0)));
1560        let t = Term::App(Box::new(id), Box::new(Term::Var(0)));
1561        let (result, steps, converged) = reducer.reduce(&t);
1562        assert!(converged);
1563        assert!(steps >= 1);
1564        assert!(reducer.is_normal_form(&result));
1565    }
1566    #[test]
1567    fn test_beta_reducer_step_count() {
1568        let reducer = BetaReducer::new(Strategy::NormalOrder, 10000);
1569        let one_plus_one = church_add(1, 1);
1570        let steps_opt = reducer.count_steps(&one_plus_one);
1571        assert!(steps_opt.is_some());
1572    }
1573    #[test]
1574    fn test_alpha_equiv_identical() {
1575        let checker = AlphaEquivalenceChecker::new();
1576        let t = Term::Lam(Box::new(Term::Var(0)));
1577        assert!(checker.alpha_equiv(&t, &t));
1578    }
1579    #[test]
1580    fn test_alpha_equiv_different() {
1581        let checker = AlphaEquivalenceChecker::new();
1582        let t1 = Term::Lam(Box::new(Term::Var(0)));
1583        let t2 = Term::Lam(Box::new(Term::Var(1)));
1584        assert!(!checker.alpha_equiv(&t1, &t2));
1585    }
1586    #[test]
1587    fn test_alpha_equiv_normalized() {
1588        let checker = AlphaEquivalenceChecker::new();
1589        let id = Term::Lam(Box::new(Term::Var(0)));
1590        let t = Term::App(Box::new(id), Box::new(Term::Var(1)));
1591        let expected = Term::Var(1);
1592        assert!(checker.alpha_equiv_normalized(&t, &expected, 100));
1593    }
1594    #[test]
1595    fn test_type_inference_var() {
1596        let system = TypeInferenceSystem::new();
1597        let alpha = SimpleType::Base("α".into());
1598        let ctx = Context(vec![alpha.clone()]);
1599        assert_eq!(system.synthesize(&ctx, &Term::Var(0)), Some(alpha));
1600    }
1601    #[test]
1602    fn test_type_inference_app() {
1603        let system = TypeInferenceSystem::new();
1604        let alpha = SimpleType::Base("α".into());
1605        let beta = SimpleType::Base("β".into());
1606        let ctx = Context(vec![
1607            alpha.clone(),
1608            SimpleType::arr(alpha.clone(), beta.clone()),
1609        ]);
1610        let term = Term::App(Box::new(Term::Var(1)), Box::new(Term::Var(0)));
1611        assert_eq!(system.synthesize(&ctx, &term), Some(beta));
1612    }
1613    #[test]
1614    fn test_type_check_identity() {
1615        let system = TypeInferenceSystem::new();
1616        let alpha = SimpleType::Base("α".into());
1617        let id = Term::Lam(Box::new(Term::Var(0)));
1618        let ctx = Context::empty();
1619        assert!(system.check(&ctx, &id, &SimpleType::arr(alpha.clone(), alpha)));
1620    }
1621    #[test]
1622    fn test_type_inference_with_hint() {
1623        let system = TypeInferenceSystem::new();
1624        let alpha = SimpleType::Base("α".into());
1625        let id = Term::Lam(Box::new(Term::Var(0)));
1626        let ty = SimpleType::arr(alpha.clone(), alpha);
1627        let ctx = Context::empty();
1628        let result = system.infer_with_annotation(&ctx, &id, Some(&ty));
1629        assert!(result.is_some());
1630    }
1631    #[test]
1632    fn test_linear_identity_is_linear() {
1633        let checker = LinearTypeChecker::new();
1634        let id = Term::Lam(Box::new(Term::Var(0)));
1635        let uses = checker.count_uses(&id, 0);
1636        assert!(uses.is_empty());
1637        let uses_body = checker.count_uses(&Term::Var(0), 1);
1638        assert_eq!(uses_body, vec![1]);
1639    }
1640    #[test]
1641    fn test_linear_k_combinator_is_not_linear() {
1642        let checker = LinearTypeChecker::new();
1643        let body = Term::Var(1);
1644        let uses = checker.count_uses(&body, 2);
1645        assert_eq!(uses, vec![0, 1]);
1646        assert!(!checker.is_linear(&body, 2));
1647        assert!(checker.is_affine(&body, 2));
1648    }
1649    #[test]
1650    fn test_affine_vs_relevant() {
1651        let checker = LinearTypeChecker::new();
1652        let body = Term::App(
1653            Box::new(Term::App(Box::new(Term::Var(1)), Box::new(Term::Var(0)))),
1654            Box::new(Term::Var(0)),
1655        );
1656        let uses = checker.count_uses(&body, 2);
1657        assert_eq!(uses, vec![2, 1]);
1658        assert!(!checker.is_linear(&body, 2));
1659        assert!(!checker.is_affine(&body, 2));
1660        assert!(checker.is_relevant(&body, 2));
1661    }
1662    #[test]
1663    fn test_session_dual_send_recv() {
1664        let compat = SessionTypeCompatibility::new();
1665        let s = BinarySession::Send("Int".into(), Box::new(BinarySession::End));
1666        let dual = compat.dual(&s);
1667        assert_eq!(
1668            dual,
1669            BinarySession::Recv("Int".into(), Box::new(BinarySession::End))
1670        );
1671    }
1672    #[test]
1673    fn test_session_dual_involutive() {
1674        let compat = SessionTypeCompatibility::new();
1675        let s = BinarySession::Send(
1676            "Bool".into(),
1677            Box::new(BinarySession::Recv(
1678                "Int".into(),
1679                Box::new(BinarySession::End),
1680            )),
1681        );
1682        let d = compat.dual(&compat.dual(&s));
1683        assert_eq!(d, s);
1684    }
1685    #[test]
1686    fn test_session_compatible_send_recv() {
1687        let compat = SessionTypeCompatibility::new();
1688        let s1 = BinarySession::Send("Int".into(), Box::new(BinarySession::End));
1689        let s2 = BinarySession::Recv("Int".into(), Box::new(BinarySession::End));
1690        assert!(compat.compatible(&s1, &s2));
1691        assert!(compat.compatible(&s2, &s1));
1692    }
1693    #[test]
1694    fn test_session_incompatible_type_mismatch() {
1695        let compat = SessionTypeCompatibility::new();
1696        let s1 = BinarySession::Send("Int".into(), Box::new(BinarySession::End));
1697        let s2 = BinarySession::Recv("Bool".into(), Box::new(BinarySession::End));
1698        assert!(!compat.compatible(&s1, &s2));
1699    }
1700    #[test]
1701    fn test_session_compatible_end_end() {
1702        let compat = SessionTypeCompatibility::new();
1703        assert!(compat.compatible(&BinarySession::End, &BinarySession::End));
1704    }
1705    #[test]
1706    fn test_session_are_dual() {
1707        let compat = SessionTypeCompatibility::new();
1708        let s1 = BinarySession::Send("Nat".into(), Box::new(BinarySession::End));
1709        let s2 = BinarySession::Recv("Nat".into(), Box::new(BinarySession::End));
1710        assert!(compat.are_dual(&s1, &s2));
1711        assert!(compat.are_dual(&s2, &s1));
1712        assert!(!compat.are_dual(&s1, &s1));
1713    }
1714    #[test]
1715    fn test_session_select_offer_compatible() {
1716        let compat = SessionTypeCompatibility::new();
1717        let s1 = BinarySession::Select(vec![
1718            ("ok".into(), BinarySession::End),
1719            ("err".into(), BinarySession::End),
1720        ]);
1721        let s2 = BinarySession::Offer(vec![
1722            ("ok".into(), BinarySession::End),
1723            ("err".into(), BinarySession::End),
1724        ]);
1725        assert!(compat.compatible(&s1, &s2));
1726    }
1727}
oxilean_std/lambda_calculus/functions.rs

oxilean_std/lambda_calculus/
functions.rs
