oxilean_std/domain_theory/
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};
6
7use super::types::{
8    AdditiveConj, AlgebraicDomain, BanachFixedPoint, BifiniteApproximation, CoherenceSpace,
9    ContinuousDomain, ContinuousLattice, Denotation, DenotationalSoundness, DomainEqn,
10    DomainEquation, EnvironmentModel, ExponentialModality, IdealCompletion, InformationSystem,
11    KleeneFixedPoint, LinearArrow, LinearType, MultiplicativeConj, OperationalEquivalence,
12    Powerdomain, PrimeEventStructure, ProofNet, ScottContinuousFunction, ScottDomain, ScottOpenSet,
13    SemanticDomain, StableFunction, DCPO,
14};
15
16pub fn app(f: Expr, a: Expr) -> Expr {
17    Expr::App(Box::new(f), Box::new(a))
18}
19pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
20    app(app(f, a), b)
21}
22pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
23    app(app2(f, a, b), c)
24}
25pub fn app4(f: Expr, a: Expr, b: Expr, c: Expr, d: Expr) -> Expr {
26    app(app3(f, a, b, c), d)
27}
28pub fn cst(s: &str) -> Expr {
29    Expr::Const(Name::str(s), vec![])
30}
31pub fn prop() -> Expr {
32    Expr::Sort(Level::zero())
33}
34pub fn type0() -> Expr {
35    Expr::Sort(Level::succ(Level::zero()))
36}
37pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
38    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
39}
40pub fn arrow(a: Expr, b: Expr) -> Expr {
41    pi(BinderInfo::Default, "_", a, b)
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 string_ty() -> Expr {
56    cst("String")
57}
58/// DCPO: directed-complete partial order.
59/// Type: Type → Prop (given a carrier type, asserts it forms a DCPO).
60pub fn dcpo_ty() -> Expr {
61    arrow(type0(), prop())
62}
63/// ScottDomain: bounded-complete DCPO with least element ⊥.
64pub fn scott_domain_ty() -> Expr {
65    arrow(type0(), prop())
66}
67/// AlgebraicDomain: DCPO where every element is the sup of compact elements below it.
68pub fn algebraic_domain_ty() -> Expr {
69    arrow(type0(), prop())
70}
71/// ContinuousDomain: DCPO where every element is the sup of elements way-below it.
72pub fn continuous_domain_ty() -> Expr {
73    arrow(type0(), prop())
74}
75/// WayBelow relation: x ≪ y.
76/// Type: {D : Type} → D → D → Prop
77pub fn way_below_ty() -> Expr {
78    pi(
79        BinderInfo::Default,
80        "D",
81        type0(),
82        pi(
83            BinderInfo::Default,
84            "x",
85            bvar(0),
86            pi(BinderInfo::Default, "y", bvar(1), prop()),
87        ),
88    )
89}
90/// Directed sup: sup of a directed set exists.
91pub fn directed_sup_ty() -> Expr {
92    prop()
93}
94/// ScottOpenSet: upper set closed under directed sups.
95pub fn scott_open_set_ty() -> Expr {
96    pi(
97        BinderInfo::Default,
98        "D",
99        type0(),
100        arrow(arrow(bvar(0), prop()), prop()),
101    )
102}
103/// ScottContinuousFunction: preserves directed sups.
104pub fn scott_continuous_fn_ty() -> Expr {
105    pi(
106        BinderInfo::Default,
107        "D",
108        type0(),
109        pi(
110            BinderInfo::Default,
111            "E",
112            type0(),
113            arrow(arrow(bvar(1), bvar(1)), prop()),
114        ),
115    )
116}
117/// LawsonTopology: coarsest topology making both identity and complement maps continuous.
118pub fn lawson_topology_ty() -> Expr {
119    arrow(type0(), prop())
120}
121/// SpectralSpace: sober T₀ space with compact open sets closed under finite intersection.
122pub fn spectral_space_ty() -> Expr {
123    arrow(type0(), prop())
124}
125/// KleeneFixedPoint: ⊔_{n≥0} fⁿ(⊥) for Scott-continuous f on a DCPO.
126pub fn kleene_fixed_point_ty() -> Expr {
127    prop()
128}
129/// BanachFixedPoint: unique fixed point of a contractive map on a complete metric space.
130pub fn banach_fixed_point_ty() -> Expr {
131    prop()
132}
133/// DomainEquation: D ≅ F(D) for a functor F.
134pub fn domain_equation_ty() -> Expr {
135    prop()
136}
137/// SolutionByPointed: bifinite / SFP domain solving D ≅ F(D).
138pub fn solution_by_pointed_ty() -> Expr {
139    prop()
140}
141/// ScottContinuousF: functor on Cpo category.
142pub fn scott_continuous_functor_ty() -> Expr {
143    prop()
144}
145/// SemanticDomain: type → domain interpreting it.
146pub fn semantic_domain_ty() -> Expr {
147    arrow(type0(), type0())
148}
149/// Denotation: ⟦e⟧ρ = semantic value.
150pub fn denotation_ty() -> Expr {
151    prop()
152}
153/// EnvironmentModel: type contexts → domains.
154pub fn environment_model_ty() -> Expr {
155    prop()
156}
157/// OperationalEquivalence: e₁ ≡ e₂ iff ∀C: C[e₁]↓ ↔ C[e₂]↓.
158pub fn operational_equivalence_ty() -> Expr {
159    prop()
160}
161/// DenotationalSoundness: ⟦e₁⟧ = ⟦e₂⟧ ⟹ e₁ ≡ e₂.
162pub fn denotational_soundness_ty() -> Expr {
163    prop()
164}
165/// LinearType: must be used exactly once.
166pub fn linear_type_ty() -> Expr {
167    arrow(type0(), prop())
168}
169/// ExponentialModality: !A — can be used any number of times.
170pub fn exponential_modality_ty() -> Expr {
171    arrow(type0(), type0())
172}
173/// MultiplicativeConj: A ⊗ B — tensor product of linear types.
174pub fn multiplicative_conj_ty() -> Expr {
175    arrow(type0(), arrow(type0(), type0()))
176}
177/// AdditiveConj: A & B — "with", shared resources.
178pub fn additive_conj_ty() -> Expr {
179    arrow(type0(), arrow(type0(), type0()))
180}
181/// LinearArrow: A ⊸ B — linear function using A exactly once.
182pub fn linear_arrow_ty() -> Expr {
183    arrow(type0(), arrow(type0(), type0()))
184}
185/// ProofNetShortcut: multiplicative proof net (combinatorial proof structure).
186pub fn proof_net_ty() -> Expr {
187    prop()
188}
189/// CPO: complete partial order (has sups for all directed subsets, but may lack ⊥).
190pub fn cpo_ty() -> Expr {
191    arrow(type0(), prop())
192}
193/// DirectedSet: a non-empty set where any two elements have an upper bound in the set.
194pub fn directed_set_ty() -> Expr {
195    pi(
196        BinderInfo::Default,
197        "D",
198        type0(),
199        arrow(arrow(bvar(0), prop()), prop()),
200    )
201}
202/// IsDirected: predicate asserting a subset is directed.
203pub fn is_directed_ty() -> Expr {
204    pi(
205        BinderInfo::Default,
206        "D",
207        type0(),
208        arrow(arrow(bvar(0), prop()), prop()),
209    )
210}
211/// UpperBound: x is an upper bound of a subset S in a poset.
212pub fn upper_bound_ty() -> Expr {
213    pi(
214        BinderInfo::Default,
215        "D",
216        type0(),
217        pi(
218            BinderInfo::Default,
219            "x",
220            bvar(0),
221            arrow(arrow(bvar(1), prop()), prop()),
222        ),
223    )
224}
225/// IsLeastUpperBound: x is the least upper bound (supremum) of S.
226pub fn is_lub_ty() -> Expr {
227    pi(
228        BinderInfo::Default,
229        "D",
230        type0(),
231        pi(
232            BinderInfo::Default,
233            "x",
234            bvar(0),
235            arrow(arrow(bvar(1), prop()), prop()),
236        ),
237    )
238}
239/// OmegaCPO: CPO where all omega-chains (indexed by Nat) have sups.
240pub fn omega_cpo_ty() -> Expr {
241    arrow(type0(), prop())
242}
243/// ChainComplete: every chain has a supremum.
244pub fn chain_complete_ty() -> Expr {
245    arrow(type0(), prop())
246}
247/// TarskiFixedPoint: every monotone function on a complete lattice has a fixed point.
248pub fn tarski_fixed_point_ty() -> Expr {
249    prop()
250}
251/// KnasterTarskiLeastFixedPoint: least pre-fixed-point of a monotone map on a CPO.
252pub fn knaster_tarski_lfp_ty() -> Expr {
253    pi(
254        BinderInfo::Default,
255        "D",
256        type0(),
257        arrow(arrow(bvar(0), bvar(0)), bvar(0)),
258    )
259}
260/// KnasterTarskiGreatestFixedPoint: greatest post-fixed-point of a monotone map.
261pub fn knaster_tarski_gfp_ty() -> Expr {
262    pi(
263        BinderInfo::Default,
264        "D",
265        type0(),
266        arrow(arrow(bvar(0), bvar(0)), bvar(0)),
267    )
268}
269/// PreFixedPoint: x is a pre-fixed-point if f(x) ≤ x.
270pub fn pre_fixed_point_ty() -> Expr {
271    pi(
272        BinderInfo::Default,
273        "D",
274        type0(),
275        pi(
276            BinderInfo::Default,
277            "f",
278            arrow(bvar(0), bvar(0)),
279            arrow(bvar(1), prop()),
280        ),
281    )
282}
283/// PostFixedPoint: x is a post-fixed-point if x ≤ f(x).
284pub fn post_fixed_point_ty() -> Expr {
285    pi(
286        BinderInfo::Default,
287        "D",
288        type0(),
289        pi(
290            BinderInfo::Default,
291            "f",
292            arrow(bvar(0), bvar(0)),
293            arrow(bvar(1), prop()),
294        ),
295    )
296}
297/// LiftedDomain: D_⊥ — adds a new bottom element to a type.
298pub fn lifted_domain_ty() -> Expr {
299    arrow(type0(), type0())
300}
301/// ProductDomain: D × E — the product of two domains (with pointwise order).
302pub fn product_domain_ty() -> Expr {
303    arrow(type0(), arrow(type0(), type0()))
304}
305/// FunctionSpaceDomain: [D → E] — the domain of Scott-continuous functions.
306pub fn function_space_domain_ty() -> Expr {
307    arrow(type0(), arrow(type0(), type0()))
308}
309/// SumDomain: D + E — the coalesced sum domain.
310pub fn sum_domain_ty() -> Expr {
311    arrow(type0(), arrow(type0(), type0()))
312}
313/// PointedDomain: D with a specified bottom element ⊥.
314pub fn pointed_domain_ty() -> Expr {
315    arrow(type0(), prop())
316}
317/// InformationSystem: (A, Con, ⊢) — Scott's information systems.
318/// Type: encodes the three-component structure as a Prop predicate.
319pub fn information_system_ty() -> Expr {
320    prop()
321}
322/// IdealCompletion: the ideal completion of a preorder gives a domain.
323pub fn ideal_completion_ty() -> Expr {
324    arrow(type0(), type0())
325}
326/// IsIdeal: a downward-closed directed subset (a Scott ideal).
327pub fn is_ideal_ty() -> Expr {
328    pi(
329        BinderInfo::Default,
330        "P",
331        type0(),
332        arrow(arrow(bvar(0), prop()), prop()),
333    )
334}
335/// ConsistentSubset: a subset S where ∃ upper bound in the ambient system.
336pub fn consistent_subset_ty() -> Expr {
337    pi(
338        BinderInfo::Default,
339        "A",
340        type0(),
341        arrow(arrow(bvar(0), prop()), prop()),
342    )
343}
344/// EntailmentRelation: a ⊢ x in an information system.
345pub fn entailment_relation_ty() -> Expr {
346    prop()
347}
348/// PlotkinPowerdomain: the Plotkin (convex) powerdomain of D.
349pub fn plotkin_powerdomain_ty() -> Expr {
350    arrow(type0(), type0())
351}
352/// SmythPowerdomain: the Smyth (upper) powerdomain — over-approximations.
353pub fn smyth_powerdomain_ty() -> Expr {
354    arrow(type0(), type0())
355}
356/// HoarePowerdomain: the Hoare (lower) powerdomain — under-approximations.
357pub fn hoare_powerdomain_ty() -> Expr {
358    arrow(type0(), type0())
359}
360/// PowerdomainInclusion: embedding of the Hoare into the Plotkin powerdomain.
361pub fn powerdomain_inclusion_ty() -> Expr {
362    prop()
363}
364/// AngularBisimulation: bisimulation for powerdomain semantics.
365pub fn angular_bisimulation_ty() -> Expr {
366    prop()
367}
368/// SFPDomain: strongly finite projection domain (a class of bifinite domains).
369pub fn sfp_domain_ty() -> Expr {
370    arrow(type0(), prop())
371}
372/// BifDomain: bifinite domain — directed colimit of finite posets.
373pub fn bif_domain_ty() -> Expr {
374    arrow(type0(), prop())
375}
376/// StableFunction: a Scott-continuous function that also preserves greatest lower bounds
377/// of compatible pairs (Berry's stability condition).
378pub fn stable_function_ty() -> Expr {
379    pi(
380        BinderInfo::Default,
381        "D",
382        type0(),
383        pi(
384            BinderInfo::Default,
385            "E",
386            type0(),
387            arrow(arrow(bvar(1), bvar(1)), prop()),
388        ),
389    )
390}
391/// BerryOrder: the stable order f ≤_s g iff ∀x y: x≤y ∧ f y defined → f x = g x.
392pub fn berry_order_ty() -> Expr {
393    pi(
394        BinderInfo::Default,
395        "D",
396        type0(),
397        pi(
398            BinderInfo::Default,
399            "E",
400            type0(),
401            pi(
402                BinderInfo::Default,
403                "f",
404                arrow(bvar(1), bvar(1)),
405                pi(BinderInfo::Default, "g", arrow(bvar(2), bvar(2)), prop()),
406            ),
407        ),
408    )
409}
410/// StronglyStableFunction: stable AND satisfies the extra coherence condition.
411pub fn strongly_stable_function_ty() -> Expr {
412    pi(
413        BinderInfo::Default,
414        "D",
415        type0(),
416        pi(
417            BinderInfo::Default,
418            "E",
419            type0(),
420            arrow(arrow(bvar(1), bvar(1)), prop()),
421        ),
422    )
423}
424/// SequentialAlgorithm: a Berry-Curien sequential algorithm (stable function representation).
425pub fn sequential_algorithm_ty() -> Expr {
426    prop()
427}
428/// EventStructure: (E, ≤, #) — events, causality, conflict relation.
429pub fn event_structure_ty() -> Expr {
430    prop()
431}
432/// StableEventStructure: event structure with stability axiom.
433pub fn stable_event_structure_ty() -> Expr {
434    prop()
435}
436/// PrimeEventStructure: event structure where causality is a forest.
437pub fn prime_event_structure_ty() -> Expr {
438    prop()
439}
440/// ConflictRelation: irreflexive symmetric relation # on events.
441pub fn conflict_relation_ty() -> Expr {
442    pi(
443        BinderInfo::Default,
444        "E",
445        type0(),
446        arrow(bvar(0), arrow(bvar(1), prop())),
447    )
448}
449/// CoherenceSpace: a set of cliques (tokens + coherence relation).
450pub fn coherence_space_ty() -> Expr {
451    prop()
452}
453/// WebOfCoherenceSpace: the underlying set of tokens.
454pub fn web_of_coherence_space_ty() -> Expr {
455    arrow(type0(), type0())
456}
457/// CliqueFunctionSpace: A → B for coherence spaces A and B.
458pub fn clique_function_space_ty() -> Expr {
459    arrow(type0(), arrow(type0(), type0()))
460}
461/// GameArena: (P, O, λ, ⊢) — a two-player game for game semantics.
462pub fn game_arena_ty() -> Expr {
463    prop()
464}
465/// GameStrategy: a deterministic strategy in a game arena.
466pub fn game_strategy_ty() -> Expr {
467    prop()
468}
469/// InnocentStrategy: a strategy that only depends on P-view (locally determined).
470pub fn innocent_strategy_ty() -> Expr {
471    prop()
472}
473/// WellBracketedStrategy: a strategy respecting call-return matching.
474pub fn well_bracketed_strategy_ty() -> Expr {
475    prop()
476}
477/// PCFType: a type in the language PCF (parallel control flow).
478pub fn pcf_type_ty() -> Expr {
479    arrow(nat_ty(), prop())
480}
481/// PCFDenotation: semantic interpretation [[e]] of a PCF term.
482pub fn pcf_denotation_ty() -> Expr {
483    prop()
484}
485/// FullAbstractionPCF: Scott's model of PCF is not fully abstract.
486pub fn full_abstraction_pcf_ty() -> Expr {
487    prop()
488}
489/// UniversalDomain: a domain D such that every domain embeds into D.
490pub fn universal_domain_ty() -> Expr {
491    prop()
492}
493/// ComputabilityInDomains: a domain-theoretic model of TTE computability.
494pub fn computability_in_domains_ty() -> Expr {
495    prop()
496}
497/// QuasimetricSpace: an asymmetric metric space (d(x,y) ≠ d(y,x) allowed).
498pub fn quasimetric_space_ty() -> Expr {
499    arrow(type0(), prop())
500}
501/// PartialEquivalenceRelation: PER used for domain-theoretic semantics of types.
502pub fn per_ty() -> Expr {
503    pi(
504        BinderInfo::Default,
505        "D",
506        type0(),
507        arrow(bvar(0), arrow(bvar(1), prop())),
508    )
509}
510/// SoberSpace: a topological space where every completely prime filter is a point.
511pub fn sober_space_ty() -> Expr {
512    arrow(type0(), prop())
513}
514/// TopologicalDomain: a domain with a compatible topology (T_0 sober space).
515pub fn topological_domain_ty() -> Expr {
516    arrow(type0(), prop())
517}
518/// DomainRetract: D is a retract of E (r∘s = id_D, s∘r ≤ id_E).
519pub fn domain_retract_ty() -> Expr {
520    pi(BinderInfo::Default, "D", type0(), arrow(type0(), prop()))
521}
522/// EmbeddingProjectionPair: (e, p) with p∘e = id and e∘p ≤ id.
523pub fn embedding_projection_pair_ty() -> Expr {
524    pi(
525        BinderInfo::Default,
526        "D",
527        type0(),
528        pi(
529            BinderInfo::Default,
530            "E",
531            type0(),
532            arrow(
533                arrow(bvar(1), bvar(1)),
534                arrow(arrow(bvar(2), bvar(2)), prop()),
535            ),
536        ),
537    )
538}
539/// DomainInverseLimit: solution of a domain equation via inverse limit construction.
540pub fn domain_inverse_limit_ty() -> Expr {
541    prop()
542}
543/// Register all domain theory axioms in the kernel environment.
544pub fn build_domain_theory_env(env: &mut Environment) -> Result<(), String> {
545    let axioms: &[(&str, Expr)] = &[
546        ("DCPO", dcpo_ty()),
547        ("ScottDomain", scott_domain_ty()),
548        ("AlgebraicDomain", algebraic_domain_ty()),
549        ("ContinuousDomain", continuous_domain_ty()),
550        ("WayBelow", way_below_ty()),
551        ("DirectedSup", directed_sup_ty()),
552        ("IsCompactElement", arrow(type0(), arrow(type0(), prop()))),
553        ("HasBottom", arrow(type0(), prop())),
554        ("HasTop", arrow(type0(), prop())),
555        ("Sup", arrow(list_ty(type0()), type0())),
556        ("ScottOpenSet", scott_open_set_ty()),
557        ("ScottContinuousFunction", scott_continuous_fn_ty()),
558        ("LawsonTopology", lawson_topology_ty()),
559        ("SpectralSpace", spectral_space_ty()),
560        ("IsScottOpen", prop()),
561        ("IsScottClosed", prop()),
562        ("KleeneFixedPoint", kleene_fixed_point_ty()),
563        ("BanachFixedPoint", banach_fixed_point_ty()),
564        ("DomainEquation", domain_equation_ty()),
565        ("SolutionByPointed", solution_by_pointed_ty()),
566        ("ScottContinuousFunctor", scott_continuous_functor_ty()),
567        ("KleeneChain", prop()),
568        ("DomainIsomorphism", prop()),
569        ("SemanticDomain", semantic_domain_ty()),
570        ("Denotation", denotation_ty()),
571        ("EnvironmentModel", environment_model_ty()),
572        ("OperationalEquivalence", operational_equivalence_ty()),
573        ("DenotationalSoundness", denotational_soundness_ty()),
574        ("DenotationalAdequacy", prop()),
575        ("FullAbstraction", prop()),
576        ("LinearType", linear_type_ty()),
577        ("ExponentialModality", exponential_modality_ty()),
578        ("MultiplicativeConj", multiplicative_conj_ty()),
579        ("AdditiveConj", additive_conj_ty()),
580        ("LinearArrow", linear_arrow_ty()),
581        ("ProofNet", proof_net_ty()),
582        (
583            "MultiplicativeDisj",
584            arrow(type0(), arrow(type0(), type0())),
585        ),
586        ("AdditiveDisj", arrow(type0(), arrow(type0(), type0()))),
587        ("LinearNeg", arrow(type0(), type0())),
588        ("CutElimination", prop()),
589        ("CPO", cpo_ty()),
590        ("DirectedSet", directed_set_ty()),
591        ("IsDirected", is_directed_ty()),
592        ("UpperBound", upper_bound_ty()),
593        ("IsLeastUpperBound", is_lub_ty()),
594        ("OmegaCPO", omega_cpo_ty()),
595        ("ChainComplete", chain_complete_ty()),
596        ("TarskiFixedPoint", tarski_fixed_point_ty()),
597        ("KnasterTarskiLFP", knaster_tarski_lfp_ty()),
598        ("KnasterTarskiGFP", knaster_tarski_gfp_ty()),
599        ("PreFixedPoint", pre_fixed_point_ty()),
600        ("PostFixedPoint", post_fixed_point_ty()),
601        ("LiftedDomain", lifted_domain_ty()),
602        ("ProductDomain", product_domain_ty()),
603        ("FunctionSpaceDomain", function_space_domain_ty()),
604        ("SumDomain", sum_domain_ty()),
605        ("PointedDomain", pointed_domain_ty()),
606        ("InformationSystem", information_system_ty()),
607        ("IdealCompletion", ideal_completion_ty()),
608        ("IsIdeal", is_ideal_ty()),
609        ("ConsistentSubset", consistent_subset_ty()),
610        ("EntailmentRelation", entailment_relation_ty()),
611        ("PlotkinPowerdomain", plotkin_powerdomain_ty()),
612        ("SmythPowerdomain", smyth_powerdomain_ty()),
613        ("HoarePowerdomain", hoare_powerdomain_ty()),
614        ("PowerdomainInclusion", powerdomain_inclusion_ty()),
615        ("AngularBisimulation", angular_bisimulation_ty()),
616        ("SFPDomain", sfp_domain_ty()),
617        ("BifDomain", bif_domain_ty()),
618        ("StableFunction", stable_function_ty()),
619        ("BerryOrder", berry_order_ty()),
620        ("StronglyStableFunction", strongly_stable_function_ty()),
621        ("SequentialAlgorithm", sequential_algorithm_ty()),
622        ("EventStructure", event_structure_ty()),
623        ("StableEventStructure", stable_event_structure_ty()),
624        ("PrimeEventStructure", prime_event_structure_ty()),
625        ("ConflictRelation", conflict_relation_ty()),
626        ("CoherenceSpace", coherence_space_ty()),
627        ("WebOfCoherenceSpace", web_of_coherence_space_ty()),
628        ("CliqueFunctionSpace", clique_function_space_ty()),
629        ("GameArena", game_arena_ty()),
630        ("GameStrategy", game_strategy_ty()),
631        ("InnocentStrategy", innocent_strategy_ty()),
632        ("WellBracketedStrategy", well_bracketed_strategy_ty()),
633        ("PCFType", pcf_type_ty()),
634        ("PCFDenotation", pcf_denotation_ty()),
635        ("FullAbstractionPCF", full_abstraction_pcf_ty()),
636        ("UniversalDomain", universal_domain_ty()),
637        ("ComputabilityInDomains", computability_in_domains_ty()),
638        ("QuasimetricSpace", quasimetric_space_ty()),
639        ("PartialEquivalenceRelation", per_ty()),
640        ("SoberSpace", sober_space_ty()),
641        ("TopologicalDomain", topological_domain_ty()),
642        ("DomainRetract", domain_retract_ty()),
643        ("EmbeddingProjectionPair", embedding_projection_pair_ty()),
644        ("DomainInverseLimit", domain_inverse_limit_ty()),
645    ];
646    for (name, ty) in axioms {
647        env.add(Declaration::Axiom {
648            name: Name::str(*name),
649            univ_params: vec![],
650            ty: ty.clone(),
651        })
652        .ok();
653    }
654    Ok(())
655}
656#[cfg(test)]
657mod tests_domain_theory_ext {
658    use super::*;
659    #[test]
660    fn test_continuous_lattice() {
661        let cl = ContinuousLattice::new("L", true);
662        assert!(cl.is_algebraic);
663        assert!(cl.interpolation_property());
664        let desc = cl.way_below_description();
665        assert!(desc.contains("≪"));
666        let ir = ContinuousLattice::real_interval_domain();
667        assert!(!ir.is_algebraic);
668        let scott = ir.scott_topology_description();
669        assert!(scott.contains("Scott"));
670    }
671    #[test]
672    fn test_information_system() {
673        let mut is =
674            InformationSystem::new(vec!["a".to_string(), "b".to_string(), "c".to_string()]);
675        is.add_consistent(0, 1);
676        is.add_consistent(1, 2);
677        is.add_entailment(vec![0, 1], 2);
678        assert!(is.is_consistent_set(&[0, 1]));
679        assert!(!is.is_consistent_set(&[0, 2]));
680        let desc = is.scott_domain_from_is();
681        assert!(desc.contains("consistent"));
682    }
683    #[test]
684    fn test_powerdomains() {
685        let plotkin = Powerdomain::plotkin("D");
686        let sem = plotkin.semantics_for();
687        assert!(sem.contains("nondeterminism"));
688        let smyth = Powerdomain::smyth("D");
689        let ord = smyth.order_description();
690        assert!(ord.contains("Smyth"));
691        let hoare = Powerdomain::hoare("D");
692        let hord = hoare.order_description();
693        assert!(hord.contains("Hoare"));
694    }
695    #[test]
696    fn test_domain_equation() {
697        let uc = DomainEqn::untyped_lambda_calculus();
698        assert!(uc.solution_name.contains("Scott"));
699        let desc = uc.banach_iteration_description();
700        assert!(desc.contains("Banach"));
701        let stream = DomainEqn::recursive_stream();
702        assert!(stream.variable == "S");
703        let pitts = stream.pitts_theorem();
704        assert!(pitts.contains("Pitts"));
705    }
706    #[test]
707    fn test_bifinite_approximation() {
708        let mut ba = BifiniteApproximation::new("D∞");
709        ba.add_level("D0");
710        ba.add_level("D1");
711        ba.add_level("D2");
712        assert!(ba.is_sfp_domain());
713        let col = ba.colimit_description();
714        assert!(col.contains("D0 → D1 → D2"));
715    }
716}
oxilean_std/domain_theory/functions.rs

oxilean_std/domain_theory/
functions.rs
