oxilean_std/stream/
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::{LazyStream, StreamDeclStats};
8
9/// Build Stream type in the environment.
10pub fn build_stream_env(env: &mut Environment) -> Result<(), String> {
11    let type1 = Expr::Sort(Level::succ(Level::zero()));
12    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
13    let stream_ty = Expr::Pi(
14        BinderInfo::Default,
15        Name::str("α"),
16        Box::new(type1.clone()),
17        Box::new(type2.clone()),
18    );
19    env.add(Declaration::Axiom {
20        name: Name::str("Stream"),
21        univ_params: vec![],
22        ty: stream_ty,
23    })
24    .map_err(|e| e.to_string())?;
25    let cons_ty = Expr::Pi(
26        BinderInfo::Implicit,
27        Name::str("α"),
28        Box::new(type1.clone()),
29        Box::new(Expr::Pi(
30            BinderInfo::Default,
31            Name::str("head"),
32            Box::new(Expr::BVar(0)),
33            Box::new(Expr::Pi(
34                BinderInfo::Default,
35                Name::str("tail"),
36                Box::new(Expr::App(
37                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
38                    Box::new(Expr::BVar(1)),
39                )),
40                Box::new(Expr::App(
41                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
42                    Box::new(Expr::BVar(2)),
43                )),
44            )),
45        )),
46    );
47    env.add(Declaration::Axiom {
48        name: Name::str("Stream.cons"),
49        univ_params: vec![],
50        ty: cons_ty,
51    })
52    .map_err(|e| e.to_string())?;
53    let head_ty = Expr::Pi(
54        BinderInfo::Implicit,
55        Name::str("α"),
56        Box::new(type1.clone()),
57        Box::new(Expr::Pi(
58            BinderInfo::Default,
59            Name::str("s"),
60            Box::new(Expr::App(
61                Box::new(Expr::Const(Name::str("Stream"), vec![])),
62                Box::new(Expr::BVar(0)),
63            )),
64            Box::new(Expr::BVar(1)),
65        )),
66    );
67    env.add(Declaration::Axiom {
68        name: Name::str("Stream.head"),
69        univ_params: vec![],
70        ty: head_ty,
71    })
72    .map_err(|e| e.to_string())?;
73    let tail_ty = Expr::Pi(
74        BinderInfo::Implicit,
75        Name::str("α"),
76        Box::new(type1.clone()),
77        Box::new(Expr::Pi(
78            BinderInfo::Default,
79            Name::str("s"),
80            Box::new(Expr::App(
81                Box::new(Expr::Const(Name::str("Stream"), vec![])),
82                Box::new(Expr::BVar(0)),
83            )),
84            Box::new(Expr::App(
85                Box::new(Expr::Const(Name::str("Stream"), vec![])),
86                Box::new(Expr::BVar(1)),
87            )),
88        )),
89    );
90    env.add(Declaration::Axiom {
91        name: Name::str("Stream.tail"),
92        univ_params: vec![],
93        ty: tail_ty,
94    })
95    .map_err(|e| e.to_string())?;
96    let map_ty = Expr::Pi(
97        BinderInfo::Implicit,
98        Name::str("α"),
99        Box::new(type1.clone()),
100        Box::new(Expr::Pi(
101            BinderInfo::Implicit,
102            Name::str("β"),
103            Box::new(type1.clone()),
104            Box::new(Expr::Pi(
105                BinderInfo::Default,
106                Name::str("f"),
107                Box::new(Expr::Pi(
108                    BinderInfo::Default,
109                    Name::str("_"),
110                    Box::new(Expr::BVar(1)),
111                    Box::new(Expr::BVar(1)),
112                )),
113                Box::new(Expr::Pi(
114                    BinderInfo::Default,
115                    Name::str("s"),
116                    Box::new(Expr::App(
117                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
118                        Box::new(Expr::BVar(2)),
119                    )),
120                    Box::new(Expr::App(
121                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
122                        Box::new(Expr::BVar(2)),
123                    )),
124                )),
125            )),
126        )),
127    );
128    env.add(Declaration::Axiom {
129        name: Name::str("Stream.map"),
130        univ_params: vec![],
131        ty: map_ty,
132    })
133    .map_err(|e| e.to_string())?;
134    let take_ty = Expr::Pi(
135        BinderInfo::Implicit,
136        Name::str("α"),
137        Box::new(type1.clone()),
138        Box::new(Expr::Pi(
139            BinderInfo::Default,
140            Name::str("n"),
141            Box::new(Expr::Const(Name::str("Nat"), vec![])),
142            Box::new(Expr::Pi(
143                BinderInfo::Default,
144                Name::str("s"),
145                Box::new(Expr::App(
146                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
147                    Box::new(Expr::BVar(1)),
148                )),
149                Box::new(Expr::App(
150                    Box::new(Expr::Const(Name::str("List"), vec![])),
151                    Box::new(Expr::BVar(2)),
152                )),
153            )),
154        )),
155    );
156    env.add(Declaration::Axiom {
157        name: Name::str("Stream.take"),
158        univ_params: vec![],
159        ty: take_ty,
160    })
161    .map_err(|e| e.to_string())?;
162    Ok(())
163}
164#[cfg(test)]
165mod tests {
166    use super::*;
167    fn setup_env() -> Environment {
168        let mut env = Environment::new();
169        let type1 = Expr::Sort(Level::succ(Level::zero()));
170        let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
171        env.add(Declaration::Axiom {
172            name: Name::str("Nat"),
173            univ_params: vec![],
174            ty: type1.clone(),
175        })
176        .expect("operation should succeed");
177        let list_ty = Expr::Pi(
178            BinderInfo::Default,
179            Name::str("α"),
180            Box::new(type1),
181            Box::new(type2),
182        );
183        env.add(Declaration::Axiom {
184            name: Name::str("List"),
185            univ_params: vec![],
186            ty: list_ty,
187        })
188        .expect("operation should succeed");
189        env
190    }
191    #[test]
192    fn test_build_stream_env() {
193        let mut env = setup_env();
194        assert!(build_stream_env(&mut env).is_ok());
195        assert!(env.get(&Name::str("Stream")).is_some());
196        assert!(env.get(&Name::str("Stream.cons")).is_some());
197    }
198    #[test]
199    fn test_stream_head() {
200        let mut env = setup_env();
201        build_stream_env(&mut env).expect("build_stream_env should succeed");
202        let decl = env
203            .get(&Name::str("Stream.head"))
204            .expect("declaration 'Stream.head' should exist in env");
205        assert!(matches!(decl, Declaration::Axiom { .. }));
206    }
207    #[test]
208    fn test_stream_tail() {
209        let mut env = setup_env();
210        build_stream_env(&mut env).expect("build_stream_env should succeed");
211        let decl = env
212            .get(&Name::str("Stream.tail"))
213            .expect("declaration 'Stream.tail' should exist in env");
214        assert!(matches!(decl, Declaration::Axiom { .. }));
215    }
216    #[test]
217    fn test_stream_map() {
218        let mut env = setup_env();
219        build_stream_env(&mut env).expect("build_stream_env should succeed");
220        let decl = env
221            .get(&Name::str("Stream.map"))
222            .expect("declaration 'Stream.map' should exist in env");
223        assert!(matches!(decl, Declaration::Axiom { .. }));
224    }
225    #[test]
226    fn test_stream_take() {
227        let mut env = setup_env();
228        build_stream_env(&mut env).expect("build_stream_env should succeed");
229        let decl = env
230            .get(&Name::str("Stream.take"))
231            .expect("declaration 'Stream.take' should exist in env");
232        assert!(matches!(decl, Declaration::Axiom { .. }));
233    }
234}
235/// Build extended Stream combinators in the environment.
236///
237/// Adds `zip`, `filter`, `iterate`, `drop`, `nth`, and `zipWith`.
238pub fn build_stream_combinators(env: &mut Environment) -> Result<(), String> {
239    let type1 = Expr::Sort(Level::succ(Level::zero()));
240    let zip_ty = Expr::Pi(
241        BinderInfo::Implicit,
242        Name::str("α"),
243        Box::new(type1.clone()),
244        Box::new(Expr::Pi(
245            BinderInfo::Implicit,
246            Name::str("β"),
247            Box::new(type1.clone()),
248            Box::new(Expr::Pi(
249                BinderInfo::Default,
250                Name::str("s1"),
251                Box::new(Expr::App(
252                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
253                    Box::new(Expr::BVar(1)),
254                )),
255                Box::new(Expr::Pi(
256                    BinderInfo::Default,
257                    Name::str("s2"),
258                    Box::new(Expr::App(
259                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
260                        Box::new(Expr::BVar(1)),
261                    )),
262                    Box::new(Expr::App(
263                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
264                        Box::new(Expr::App(
265                            Box::new(Expr::App(
266                                Box::new(Expr::Const(Name::str("Prod"), vec![])),
267                                Box::new(Expr::BVar(3)),
268                            )),
269                            Box::new(Expr::BVar(2)),
270                        )),
271                    )),
272                )),
273            )),
274        )),
275    );
276    env.add(Declaration::Axiom {
277        name: Name::str("Stream.zip"),
278        univ_params: vec![],
279        ty: zip_ty,
280    })
281    .map_err(|e| e.to_string())?;
282    let iterate_ty = Expr::Pi(
283        BinderInfo::Implicit,
284        Name::str("α"),
285        Box::new(type1.clone()),
286        Box::new(Expr::Pi(
287            BinderInfo::Default,
288            Name::str("init"),
289            Box::new(Expr::BVar(0)),
290            Box::new(Expr::Pi(
291                BinderInfo::Default,
292                Name::str("step"),
293                Box::new(Expr::Pi(
294                    BinderInfo::Default,
295                    Name::str("_"),
296                    Box::new(Expr::BVar(1)),
297                    Box::new(Expr::BVar(1)),
298                )),
299                Box::new(Expr::App(
300                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
301                    Box::new(Expr::BVar(2)),
302                )),
303            )),
304        )),
305    );
306    env.add(Declaration::Axiom {
307        name: Name::str("Stream.iterate"),
308        univ_params: vec![],
309        ty: iterate_ty,
310    })
311    .map_err(|e| e.to_string())?;
312    let drop_ty = Expr::Pi(
313        BinderInfo::Implicit,
314        Name::str("α"),
315        Box::new(type1.clone()),
316        Box::new(Expr::Pi(
317            BinderInfo::Default,
318            Name::str("n"),
319            Box::new(Expr::Const(Name::str("Nat"), vec![])),
320            Box::new(Expr::Pi(
321                BinderInfo::Default,
322                Name::str("s"),
323                Box::new(Expr::App(
324                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
325                    Box::new(Expr::BVar(1)),
326                )),
327                Box::new(Expr::App(
328                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
329                    Box::new(Expr::BVar(2)),
330                )),
331            )),
332        )),
333    );
334    env.add(Declaration::Axiom {
335        name: Name::str("Stream.drop"),
336        univ_params: vec![],
337        ty: drop_ty,
338    })
339    .map_err(|e| e.to_string())?;
340    let nth_ty = Expr::Pi(
341        BinderInfo::Implicit,
342        Name::str("α"),
343        Box::new(type1.clone()),
344        Box::new(Expr::Pi(
345            BinderInfo::Default,
346            Name::str("n"),
347            Box::new(Expr::Const(Name::str("Nat"), vec![])),
348            Box::new(Expr::Pi(
349                BinderInfo::Default,
350                Name::str("s"),
351                Box::new(Expr::App(
352                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
353                    Box::new(Expr::BVar(1)),
354                )),
355                Box::new(Expr::BVar(2)),
356            )),
357        )),
358    );
359    env.add(Declaration::Axiom {
360        name: Name::str("Stream.nth"),
361        univ_params: vec![],
362        ty: nth_ty,
363    })
364    .map_err(|e| e.to_string())?;
365    let const_ty = Expr::Pi(
366        BinderInfo::Implicit,
367        Name::str("α"),
368        Box::new(type1.clone()),
369        Box::new(Expr::Pi(
370            BinderInfo::Default,
371            Name::str("val"),
372            Box::new(Expr::BVar(0)),
373            Box::new(Expr::App(
374                Box::new(Expr::Const(Name::str("Stream"), vec![])),
375                Box::new(Expr::BVar(1)),
376            )),
377        )),
378    );
379    env.add(Declaration::Axiom {
380        name: Name::str("Stream.const"),
381        univ_params: vec![],
382        ty: const_ty,
383    })
384    .map_err(|e| e.to_string())?;
385    let filter_ty = Expr::Pi(
386        BinderInfo::Implicit,
387        Name::str("α"),
388        Box::new(type1.clone()),
389        Box::new(Expr::Pi(
390            BinderInfo::Default,
391            Name::str("pred"),
392            Box::new(Expr::Pi(
393                BinderInfo::Default,
394                Name::str("_"),
395                Box::new(Expr::BVar(0)),
396                Box::new(Expr::Const(Name::str("Bool"), vec![])),
397            )),
398            Box::new(Expr::Pi(
399                BinderInfo::Default,
400                Name::str("s"),
401                Box::new(Expr::App(
402                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
403                    Box::new(Expr::BVar(1)),
404                )),
405                Box::new(Expr::App(
406                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
407                    Box::new(Expr::BVar(2)),
408                )),
409            )),
410        )),
411    );
412    env.add(Declaration::Axiom {
413        name: Name::str("Stream.filter"),
414        univ_params: vec![],
415        ty: filter_ty,
416    })
417    .map_err(|e| e.to_string())?;
418    Ok(())
419}
420#[cfg(test)]
421mod stream_combinator_tests {
422    use super::*;
423    fn setup_extended_env() -> Environment {
424        let mut env = Environment::new();
425        let type1 = Expr::Sort(Level::succ(Level::zero()));
426        let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
427        env.add(Declaration::Axiom {
428            name: Name::str("Nat"),
429            univ_params: vec![],
430            ty: type1.clone(),
431        })
432        .expect("operation should succeed");
433        env.add(Declaration::Axiom {
434            name: Name::str("Bool"),
435            univ_params: vec![],
436            ty: type1.clone(),
437        })
438        .expect("operation should succeed");
439        let list_ty = Expr::Pi(
440            BinderInfo::Default,
441            Name::str("α"),
442            Box::new(type1.clone()),
443            Box::new(type2.clone()),
444        );
445        env.add(Declaration::Axiom {
446            name: Name::str("List"),
447            univ_params: vec![],
448            ty: list_ty,
449        })
450        .expect("operation should succeed");
451        let prod_ty = Expr::Pi(
452            BinderInfo::Default,
453            Name::str("α"),
454            Box::new(type1.clone()),
455            Box::new(Expr::Pi(
456                BinderInfo::Default,
457                Name::str("β"),
458                Box::new(type1.clone()),
459                Box::new(type2.clone()),
460            )),
461        );
462        env.add(Declaration::Axiom {
463            name: Name::str("Prod"),
464            univ_params: vec![],
465            ty: prod_ty,
466        })
467        .expect("operation should succeed");
468        build_stream_env(&mut env).expect("build_stream_env should succeed");
469        env
470    }
471    #[test]
472    fn test_stream_zip() {
473        let mut env = setup_extended_env();
474        assert!(build_stream_combinators(&mut env).is_ok());
475        assert!(env.get(&Name::str("Stream.zip")).is_some());
476    }
477    #[test]
478    fn test_stream_iterate() {
479        let mut env = setup_extended_env();
480        build_stream_combinators(&mut env).expect("build_stream_combinators should succeed");
481        assert!(env.get(&Name::str("Stream.iterate")).is_some());
482    }
483    #[test]
484    fn test_stream_drop() {
485        let mut env = setup_extended_env();
486        build_stream_combinators(&mut env).expect("build_stream_combinators should succeed");
487        assert!(env.get(&Name::str("Stream.drop")).is_some());
488    }
489    #[test]
490    fn test_stream_nth() {
491        let mut env = setup_extended_env();
492        build_stream_combinators(&mut env).expect("build_stream_combinators should succeed");
493        assert!(env.get(&Name::str("Stream.nth")).is_some());
494    }
495    #[test]
496    fn test_stream_const() {
497        let mut env = setup_extended_env();
498        build_stream_combinators(&mut env).expect("build_stream_combinators should succeed");
499        assert!(env.get(&Name::str("Stream.const")).is_some());
500    }
501    #[test]
502    fn test_stream_filter() {
503        let mut env = setup_extended_env();
504        build_stream_combinators(&mut env).expect("build_stream_combinators should succeed");
505        assert!(env.get(&Name::str("Stream.filter")).is_some());
506    }
507    #[test]
508    fn test_lazy_stream_constant() {
509        let mut s = LazyStream::constant(42u64);
510        assert_eq!(s.next(), Some(42));
511        assert_eq!(s.next(), Some(42));
512        assert_eq!(s.next(), Some(42));
513    }
514    #[test]
515    fn test_lazy_stream_iterate() {
516        let s = LazyStream::iterate(0u64, |x| x + 1);
517        let vals = s.take(5);
518        assert_eq!(vals, vec![0, 1, 2, 3, 4]);
519    }
520    #[test]
521    fn test_lazy_stream_take() {
522        let s = LazyStream::constant("hello");
523        let vals = s.take(3);
524        assert_eq!(vals.len(), 3);
525        assert!(vals.iter().all(|&v| v == "hello"));
526    }
527    #[test]
528    fn test_lazy_stream_from_fn() {
529        let mut counter = 0u32;
530        let mut s = LazyStream::from_fn(move || {
531            counter += 1;
532            if counter <= 3 {
533                Some(counter)
534            } else {
535                None
536            }
537        });
538        assert_eq!(s.next(), Some(1));
539        assert_eq!(s.next(), Some(2));
540        assert_eq!(s.next(), Some(3));
541        assert_eq!(s.next(), None);
542    }
543}
544/// Build Stream theorems in the environment.
545///
546/// Adds basic stream lemmas as axioms (these would be proved in a full system).
547pub fn build_stream_theorems(env: &mut Environment) -> Result<(), String> {
548    let type1 = Expr::Sort(Level::succ(Level::zero()));
549    let prop = Expr::Sort(Level::zero());
550    let head_cons_ty = Expr::Pi(
551        BinderInfo::Implicit,
552        Name::str("α"),
553        Box::new(type1.clone()),
554        Box::new(Expr::Pi(
555            BinderInfo::Default,
556            Name::str("h"),
557            Box::new(Expr::BVar(0)),
558            Box::new(Expr::Pi(
559                BinderInfo::Default,
560                Name::str("t"),
561                Box::new(Expr::App(
562                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
563                    Box::new(Expr::BVar(1)),
564                )),
565                Box::new(prop.clone()),
566            )),
567        )),
568    );
569    env.add(Declaration::Axiom {
570        name: Name::str("Stream.head_cons"),
571        univ_params: vec![],
572        ty: head_cons_ty,
573    })
574    .map_err(|e| e.to_string())?;
575    let tail_cons_ty = Expr::Pi(
576        BinderInfo::Implicit,
577        Name::str("α"),
578        Box::new(type1.clone()),
579        Box::new(Expr::Pi(
580            BinderInfo::Default,
581            Name::str("h"),
582            Box::new(Expr::BVar(0)),
583            Box::new(Expr::Pi(
584                BinderInfo::Default,
585                Name::str("t"),
586                Box::new(Expr::App(
587                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
588                    Box::new(Expr::BVar(1)),
589                )),
590                Box::new(prop.clone()),
591            )),
592        )),
593    );
594    env.add(Declaration::Axiom {
595        name: Name::str("Stream.tail_cons"),
596        univ_params: vec![],
597        ty: tail_cons_ty,
598    })
599    .map_err(|e| e.to_string())?;
600    Ok(())
601}
602#[cfg(test)]
603mod stream_theorem_tests {
604    use super::*;
605    fn base_env() -> Environment {
606        let mut env = Environment::new();
607        let type1 = Expr::Sort(Level::succ(Level::zero()));
608        let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
609        env.add(Declaration::Axiom {
610            name: Name::str("Nat"),
611            univ_params: vec![],
612            ty: type1.clone(),
613        })
614        .expect("operation should succeed");
615        let list_ty = Expr::Pi(
616            BinderInfo::Default,
617            Name::str("α"),
618            Box::new(type1.clone()),
619            Box::new(type2.clone()),
620        );
621        env.add(Declaration::Axiom {
622            name: Name::str("List"),
623            univ_params: vec![],
624            ty: list_ty,
625        })
626        .expect("operation should succeed");
627        build_stream_env(&mut env).expect("build_stream_env should succeed");
628        env
629    }
630    #[test]
631    fn test_stream_head_cons_theorem() {
632        let mut env = base_env();
633        assert!(build_stream_theorems(&mut env).is_ok());
634        assert!(env.get(&Name::str("Stream.head_cons")).is_some());
635    }
636    #[test]
637    fn test_stream_tail_cons_theorem() {
638        let mut env = base_env();
639        build_stream_theorems(&mut env).expect("build_stream_theorems should succeed");
640        assert!(env.get(&Name::str("Stream.tail_cons")).is_some());
641    }
642    #[test]
643    fn test_stream_decl_is_axiom() {
644        let mut env = base_env();
645        build_stream_theorems(&mut env).expect("build_stream_theorems should succeed");
646        let decl = env
647            .get(&Name::str("Stream.head_cons"))
648            .expect("declaration 'Stream.head_cons' should exist in env");
649        assert!(matches!(decl, Declaration::Axiom { .. }));
650    }
651}
652/// Count how many Stream declarations are registered in an environment.
653pub fn count_stream_decls(env: &Environment) -> usize {
654    let names = [
655        "Stream",
656        "Stream.cons",
657        "Stream.head",
658        "Stream.tail",
659        "Stream.map",
660        "Stream.take",
661        "Stream.zip",
662        "Stream.iterate",
663        "Stream.drop",
664        "Stream.nth",
665        "Stream.const",
666        "Stream.filter",
667        "Stream.head_cons",
668        "Stream.tail_cons",
669    ];
670    names
671        .iter()
672        .filter(|&&n| env.get(&Name::str(n)).is_some())
673        .count()
674}
675#[cfg(test)]
676mod count_tests {
677    use super::*;
678    #[test]
679    fn test_count_stream_decls_base() {
680        let mut env = Environment::new();
681        let type1 = Expr::Sort(Level::succ(Level::zero()));
682        let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
683        env.add(Declaration::Axiom {
684            name: Name::str("Nat"),
685            univ_params: vec![],
686            ty: type1.clone(),
687        })
688        .expect("operation should succeed");
689        let list_ty = Expr::Pi(
690            BinderInfo::Default,
691            Name::str("α"),
692            Box::new(type1.clone()),
693            Box::new(type2.clone()),
694        );
695        env.add(Declaration::Axiom {
696            name: Name::str("List"),
697            univ_params: vec![],
698            ty: list_ty,
699        })
700        .expect("operation should succeed");
701        build_stream_env(&mut env).expect("build_stream_env should succeed");
702        let count = count_stream_decls(&env);
703        assert!(count >= 6);
704    }
705}
706/// Build Stream monad operations in the environment.
707///
708/// Adds `Stream.pure`, `Stream.bind`, `Stream.ap`, `Stream.zipWith`,
709/// `Stream.scan`, and `Stream.interleave`.
710pub fn build_stream_monad(env: &mut Environment) -> Result<(), String> {
711    let type1 = Expr::Sort(Level::succ(Level::zero()));
712    let pure_ty = Expr::Pi(
713        BinderInfo::Implicit,
714        Name::str("α"),
715        Box::new(type1.clone()),
716        Box::new(Expr::Pi(
717            BinderInfo::Default,
718            Name::str("a"),
719            Box::new(Expr::BVar(0)),
720            Box::new(Expr::App(
721                Box::new(Expr::Const(Name::str("Stream"), vec![])),
722                Box::new(Expr::BVar(1)),
723            )),
724        )),
725    );
726    env.add(Declaration::Axiom {
727        name: Name::str("Stream.pure"),
728        univ_params: vec![],
729        ty: pure_ty,
730    })
731    .map_err(|e| e.to_string())?;
732    let scan_ty = Expr::Pi(
733        BinderInfo::Implicit,
734        Name::str("α"),
735        Box::new(type1.clone()),
736        Box::new(Expr::Pi(
737            BinderInfo::Implicit,
738            Name::str("β"),
739            Box::new(type1.clone()),
740            Box::new(Expr::Pi(
741                BinderInfo::Default,
742                Name::str("f"),
743                Box::new(Expr::Pi(
744                    BinderInfo::Default,
745                    Name::str("_"),
746                    Box::new(Expr::BVar(1)),
747                    Box::new(Expr::Pi(
748                        BinderInfo::Default,
749                        Name::str("_"),
750                        Box::new(Expr::BVar(2)),
751                        Box::new(Expr::BVar(2)),
752                    )),
753                )),
754                Box::new(Expr::Pi(
755                    BinderInfo::Default,
756                    Name::str("init"),
757                    Box::new(Expr::BVar(2)),
758                    Box::new(Expr::Pi(
759                        BinderInfo::Default,
760                        Name::str("s"),
761                        Box::new(Expr::App(
762                            Box::new(Expr::Const(Name::str("Stream"), vec![])),
763                            Box::new(Expr::BVar(3)),
764                        )),
765                        Box::new(Expr::App(
766                            Box::new(Expr::Const(Name::str("Stream"), vec![])),
767                            Box::new(Expr::BVar(3)),
768                        )),
769                    )),
770                )),
771            )),
772        )),
773    );
774    env.add(Declaration::Axiom {
775        name: Name::str("Stream.scan"),
776        univ_params: vec![],
777        ty: scan_ty,
778    })
779    .map_err(|e| e.to_string())?;
780    let interleave_ty = Expr::Pi(
781        BinderInfo::Implicit,
782        Name::str("α"),
783        Box::new(type1.clone()),
784        Box::new(Expr::Pi(
785            BinderInfo::Default,
786            Name::str("s1"),
787            Box::new(Expr::App(
788                Box::new(Expr::Const(Name::str("Stream"), vec![])),
789                Box::new(Expr::BVar(0)),
790            )),
791            Box::new(Expr::Pi(
792                BinderInfo::Default,
793                Name::str("s2"),
794                Box::new(Expr::App(
795                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
796                    Box::new(Expr::BVar(1)),
797                )),
798                Box::new(Expr::App(
799                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
800                    Box::new(Expr::BVar(2)),
801                )),
802            )),
803        )),
804    );
805    env.add(Declaration::Axiom {
806        name: Name::str("Stream.interleave"),
807        univ_params: vec![],
808        ty: interleave_ty,
809    })
810    .map_err(|e| e.to_string())?;
811    Ok(())
812}
813#[cfg(test)]
814mod stream_monad_tests {
815    use super::*;
816    fn full_env() -> Environment {
817        let mut env = Environment::new();
818        let type1 = Expr::Sort(Level::succ(Level::zero()));
819        let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
820        env.add(Declaration::Axiom {
821            name: Name::str("Nat"),
822            univ_params: vec![],
823            ty: type1.clone(),
824        })
825        .expect("operation should succeed");
826        env.add(Declaration::Axiom {
827            name: Name::str("Bool"),
828            univ_params: vec![],
829            ty: type1.clone(),
830        })
831        .expect("operation should succeed");
832        env.add(Declaration::Axiom {
833            name: Name::str("List"),
834            univ_params: vec![],
835            ty: Expr::Pi(
836                BinderInfo::Default,
837                Name::str("α"),
838                Box::new(type1.clone()),
839                Box::new(type2.clone()),
840            ),
841        })
842        .expect("operation should succeed");
843        env.add(Declaration::Axiom {
844            name: Name::str("Prod"),
845            univ_params: vec![],
846            ty: Expr::Pi(
847                BinderInfo::Default,
848                Name::str("α"),
849                Box::new(type1.clone()),
850                Box::new(Expr::Pi(
851                    BinderInfo::Default,
852                    Name::str("β"),
853                    Box::new(type1.clone()),
854                    Box::new(type2.clone()),
855                )),
856            ),
857        })
858        .expect("operation should succeed");
859        build_stream_env(&mut env).expect("build_stream_env should succeed");
860        env
861    }
862    #[test]
863    fn test_stream_pure() {
864        let mut env = full_env();
865        build_stream_monad(&mut env).expect("build_stream_monad should succeed");
866        assert!(env.get(&Name::str("Stream.pure")).is_some());
867    }
868    #[test]
869    fn test_stream_scan() {
870        let mut env = full_env();
871        build_stream_monad(&mut env).expect("build_stream_monad should succeed");
872        assert!(env.get(&Name::str("Stream.scan")).is_some());
873    }
874    #[test]
875    fn test_stream_interleave() {
876        let mut env = full_env();
877        build_stream_monad(&mut env).expect("build_stream_monad should succeed");
878        assert!(env.get(&Name::str("Stream.interleave")).is_some());
879    }
880    #[test]
881    fn test_stream_decl_stats_core() {
882        let env = full_env();
883        let stats = StreamDeclStats::compute(&env);
884        assert_eq!(stats.core, 4);
885    }
886    #[test]
887    fn test_stream_decl_stats_total() {
888        let mut env = full_env();
889        build_stream_combinators(&mut env).expect("build_stream_combinators should succeed");
890        build_stream_monad(&mut env).expect("build_stream_monad should succeed");
891        build_stream_theorems(&mut env).expect("build_stream_theorems should succeed");
892        let stats = StreamDeclStats::compute(&env);
893        assert!(stats.total() > 10);
894    }
895    #[test]
896    fn test_lazy_stream_powers_of_two() {
897        let s = LazyStream::iterate(1u64, |x| x * 2);
898        let vals = s.take(8);
899        assert_eq!(vals, vec![1, 2, 4, 8, 16, 32, 64, 128]);
900    }
901    #[test]
902    fn test_lazy_stream_from_fn_terminates() {
903        let mut s = LazyStream::from_fn(move || None::<i32>);
904        assert_eq!(s.next(), None);
905    }
906}
907/// `Stream.Bisim`: the bisimulation relation between two streams.
908/// Type: {α : Type} → Stream α → Stream α → Prop
909pub fn strm_ext_bisim_ty() -> Expr {
910    let type1 = Expr::Sort(Level::succ(Level::zero()));
911    let prop = Expr::Sort(Level::zero());
912    Expr::Pi(
913        BinderInfo::Implicit,
914        Name::str("α"),
915        Box::new(type1),
916        Box::new(Expr::Pi(
917            BinderInfo::Default,
918            Name::str("s1"),
919            Box::new(Expr::App(
920                Box::new(Expr::Const(Name::str("Stream"), vec![])),
921                Box::new(Expr::BVar(0)),
922            )),
923            Box::new(Expr::Pi(
924                BinderInfo::Default,
925                Name::str("s2"),
926                Box::new(Expr::App(
927                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
928                    Box::new(Expr::BVar(1)),
929                )),
930                Box::new(prop),
931            )),
932        )),
933    )
934}
935/// `Stream.bisim_coind`: coinductive bisimulation principle.
936/// Type: {α : Type} → (R : Stream α → Stream α → Prop) → ... → ∀ s t, R s t → s = t
937pub fn strm_ext_bisim_coind_ty() -> Expr {
938    let type1 = Expr::Sort(Level::succ(Level::zero()));
939    let prop = Expr::Sort(Level::zero());
940    Expr::Pi(
941        BinderInfo::Implicit,
942        Name::str("α"),
943        Box::new(type1),
944        Box::new(Expr::Pi(
945            BinderInfo::Default,
946            Name::str("R"),
947            Box::new(Expr::Pi(
948                BinderInfo::Default,
949                Name::str("_"),
950                Box::new(Expr::App(
951                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
952                    Box::new(Expr::BVar(0)),
953                )),
954                Box::new(Expr::Pi(
955                    BinderInfo::Default,
956                    Name::str("_"),
957                    Box::new(Expr::App(
958                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
959                        Box::new(Expr::BVar(1)),
960                    )),
961                    Box::new(prop.clone()),
962                )),
963            )),
964            Box::new(prop.clone()),
965        )),
966    )
967}
968/// `Stream.corec`: corecursion principle for streams.
969/// Type: {α σ : Type} → (σ → α) → (σ → σ) → σ → Stream α
970pub fn strm_ext_corec_ty() -> Expr {
971    let type1 = Expr::Sort(Level::succ(Level::zero()));
972    Expr::Pi(
973        BinderInfo::Implicit,
974        Name::str("α"),
975        Box::new(type1.clone()),
976        Box::new(Expr::Pi(
977            BinderInfo::Implicit,
978            Name::str("σ"),
979            Box::new(type1.clone()),
980            Box::new(Expr::Pi(
981                BinderInfo::Default,
982                Name::str("hd"),
983                Box::new(Expr::Pi(
984                    BinderInfo::Default,
985                    Name::str("_"),
986                    Box::new(Expr::BVar(0)),
987                    Box::new(Expr::BVar(1)),
988                )),
989                Box::new(Expr::Pi(
990                    BinderInfo::Default,
991                    Name::str("tl"),
992                    Box::new(Expr::Pi(
993                        BinderInfo::Default,
994                        Name::str("_"),
995                        Box::new(Expr::BVar(1)),
996                        Box::new(Expr::BVar(1)),
997                    )),
998                    Box::new(Expr::Pi(
999                        BinderInfo::Default,
1000                        Name::str("s0"),
1001                        Box::new(Expr::BVar(2)),
1002                        Box::new(Expr::App(
1003                            Box::new(Expr::Const(Name::str("Stream"), vec![])),
1004                            Box::new(Expr::BVar(4)),
1005                        )),
1006                    )),
1007                )),
1008            )),
1009        )),
1010    )
1011}
1012/// `MealyMachine.type`: a Mealy machine as stream transducer.
1013/// Type: Type → Type → Type → Type
1014pub fn strm_ext_mealy_machine_ty() -> Expr {
1015    let type1 = Expr::Sort(Level::succ(Level::zero()));
1016    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1017    Expr::Pi(
1018        BinderInfo::Default,
1019        Name::str("S"),
1020        Box::new(type1.clone()),
1021        Box::new(Expr::Pi(
1022            BinderInfo::Default,
1023            Name::str("I"),
1024            Box::new(type1.clone()),
1025            Box::new(Expr::Pi(
1026                BinderInfo::Default,
1027                Name::str("O"),
1028                Box::new(type1.clone()),
1029                Box::new(type2),
1030            )),
1031        )),
1032    )
1033}
1034/// `MealyMachine.run`: run a Mealy machine on a stream of inputs.
1035/// Type: {S I O : Type} → MealyMachine S I O → S → Stream I → Stream O
1036pub fn strm_ext_mealy_run_ty() -> Expr {
1037    let type1 = Expr::Sort(Level::succ(Level::zero()));
1038    Expr::Pi(
1039        BinderInfo::Implicit,
1040        Name::str("S"),
1041        Box::new(type1.clone()),
1042        Box::new(Expr::Pi(
1043            BinderInfo::Implicit,
1044            Name::str("I"),
1045            Box::new(type1.clone()),
1046            Box::new(Expr::Pi(
1047                BinderInfo::Implicit,
1048                Name::str("O"),
1049                Box::new(type1.clone()),
1050                Box::new(Expr::Pi(
1051                    BinderInfo::Default,
1052                    Name::str("m"),
1053                    Box::new(Expr::Const(Name::str("MealyMachine"), vec![])),
1054                    Box::new(Expr::Pi(
1055                        BinderInfo::Default,
1056                        Name::str("s0"),
1057                        Box::new(Expr::BVar(3)),
1058                        Box::new(Expr::Pi(
1059                            BinderInfo::Default,
1060                            Name::str("inp"),
1061                            Box::new(Expr::App(
1062                                Box::new(Expr::Const(Name::str("Stream"), vec![])),
1063                                Box::new(Expr::BVar(3)),
1064                            )),
1065                            Box::new(Expr::App(
1066                                Box::new(Expr::Const(Name::str("Stream"), vec![])),
1067                                Box::new(Expr::BVar(3)),
1068                            )),
1069                        )),
1070                    )),
1071                )),
1072            )),
1073        )),
1074    )
1075}
1076/// `MooreMachine.type`: a Moore machine.
1077/// Type: Type → Type → Type → Type
1078pub fn strm_ext_moore_machine_ty() -> Expr {
1079    let type1 = Expr::Sort(Level::succ(Level::zero()));
1080    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1081    Expr::Pi(
1082        BinderInfo::Default,
1083        Name::str("S"),
1084        Box::new(type1.clone()),
1085        Box::new(Expr::Pi(
1086            BinderInfo::Default,
1087            Name::str("I"),
1088            Box::new(type1.clone()),
1089            Box::new(Expr::Pi(
1090                BinderInfo::Default,
1091                Name::str("O"),
1092                Box::new(type1.clone()),
1093                Box::new(type2),
1094            )),
1095        )),
1096    )
1097}
1098/// `KPN.channel`: a Kahn process network channel (FIFO stream).
1099/// Type: Type → Type
1100pub fn strm_ext_kpn_channel_ty() -> Expr {
1101    let type1 = Expr::Sort(Level::succ(Level::zero()));
1102    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1103    Expr::Pi(
1104        BinderInfo::Default,
1105        Name::str("α"),
1106        Box::new(type1),
1107        Box::new(type2),
1108    )
1109}
1110/// `KPN.process`: a Kahn process (reads inputs, writes outputs).
1111/// Type: {α β : Type} → Stream α → Stream β
1112pub fn strm_ext_kpn_process_ty() -> Expr {
1113    let type1 = Expr::Sort(Level::succ(Level::zero()));
1114    Expr::Pi(
1115        BinderInfo::Implicit,
1116        Name::str("α"),
1117        Box::new(type1.clone()),
1118        Box::new(Expr::Pi(
1119            BinderInfo::Implicit,
1120            Name::str("β"),
1121            Box::new(type1.clone()),
1122            Box::new(Expr::Pi(
1123                BinderInfo::Default,
1124                Name::str("inp"),
1125                Box::new(Expr::App(
1126                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1127                    Box::new(Expr::BVar(1)),
1128                )),
1129                Box::new(Expr::App(
1130                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1131                    Box::new(Expr::BVar(1)),
1132                )),
1133            )),
1134        )),
1135    )
1136}
1137/// `FRP.Behavior`: a time-varying value (FRP behavior).
1138/// Type: Type → Type
1139pub fn strm_ext_frp_behavior_ty() -> Expr {
1140    let type1 = Expr::Sort(Level::succ(Level::zero()));
1141    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1142    Expr::Pi(
1143        BinderInfo::Default,
1144        Name::str("α"),
1145        Box::new(type1),
1146        Box::new(type2),
1147    )
1148}
1149/// `FRP.Event`: a discrete stream of events with timestamps.
1150/// Type: Type → Type
1151pub fn strm_ext_frp_event_ty() -> Expr {
1152    let type1 = Expr::Sort(Level::succ(Level::zero()));
1153    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1154    Expr::Pi(
1155        BinderInfo::Default,
1156        Name::str("α"),
1157        Box::new(type1),
1158        Box::new(type2),
1159    )
1160}
1161/// `FRP.stepper`: convert a stream of events to a behavior.
1162/// Type: {α : Type} → α → Stream α → FRP.Behavior α
1163pub fn strm_ext_frp_stepper_ty() -> Expr {
1164    let type1 = Expr::Sort(Level::succ(Level::zero()));
1165    Expr::Pi(
1166        BinderInfo::Implicit,
1167        Name::str("α"),
1168        Box::new(type1.clone()),
1169        Box::new(Expr::Pi(
1170            BinderInfo::Default,
1171            Name::str("init"),
1172            Box::new(Expr::BVar(0)),
1173            Box::new(Expr::Pi(
1174                BinderInfo::Default,
1175                Name::str("evts"),
1176                Box::new(Expr::App(
1177                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1178                    Box::new(Expr::BVar(1)),
1179                )),
1180                Box::new(Expr::App(
1181                    Box::new(Expr::Const(Name::str("FRP.Behavior"), vec![])),
1182                    Box::new(Expr::BVar(2)),
1183                )),
1184            )),
1185        )),
1186    )
1187}
1188/// `Stream.diff_eq`: stream differential equation axiom.
1189/// Type: {α : Type} → (Stream α → Stream α) → Stream α → Prop
1190pub fn strm_ext_diff_eq_ty() -> Expr {
1191    let type1 = Expr::Sort(Level::succ(Level::zero()));
1192    let prop = Expr::Sort(Level::zero());
1193    Expr::Pi(
1194        BinderInfo::Implicit,
1195        Name::str("α"),
1196        Box::new(type1.clone()),
1197        Box::new(Expr::Pi(
1198            BinderInfo::Default,
1199            Name::str("F"),
1200            Box::new(Expr::Pi(
1201                BinderInfo::Default,
1202                Name::str("_"),
1203                Box::new(Expr::App(
1204                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1205                    Box::new(Expr::BVar(0)),
1206                )),
1207                Box::new(Expr::App(
1208                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1209                    Box::new(Expr::BVar(1)),
1210                )),
1211            )),
1212            Box::new(Expr::Pi(
1213                BinderInfo::Default,
1214                Name::str("s"),
1215                Box::new(Expr::App(
1216                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1217                    Box::new(Expr::BVar(1)),
1218                )),
1219                Box::new(prop),
1220            )),
1221        )),
1222    )
1223}
1224/// `Stream.productivity`: guardedness / productivity condition.
1225/// Type: {α : Type} → Stream α → Prop
1226pub fn strm_ext_productivity_ty() -> Expr {
1227    let type1 = Expr::Sort(Level::succ(Level::zero()));
1228    let prop = Expr::Sort(Level::zero());
1229    Expr::Pi(
1230        BinderInfo::Implicit,
1231        Name::str("α"),
1232        Box::new(type1),
1233        Box::new(Expr::Pi(
1234            BinderInfo::Default,
1235            Name::str("s"),
1236            Box::new(Expr::App(
1237                Box::new(Expr::Const(Name::str("Stream"), vec![])),
1238                Box::new(Expr::BVar(0)),
1239            )),
1240            Box::new(prop),
1241        )),
1242    )
1243}
1244/// `Stream.guarded_fix`: guarded fixed point / corecursion under guard.
1245/// Type: {α : Type} → (Stream α → Stream α) → Stream α
1246pub fn strm_ext_guarded_fix_ty() -> Expr {
1247    let type1 = Expr::Sort(Level::succ(Level::zero()));
1248    Expr::Pi(
1249        BinderInfo::Implicit,
1250        Name::str("α"),
1251        Box::new(type1.clone()),
1252        Box::new(Expr::Pi(
1253            BinderInfo::Default,
1254            Name::str("f"),
1255            Box::new(Expr::Pi(
1256                BinderInfo::Default,
1257                Name::str("_"),
1258                Box::new(Expr::App(
1259                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1260                    Box::new(Expr::BVar(0)),
1261                )),
1262                Box::new(Expr::App(
1263                    Box::new(Expr::Const(Name::str("Stream"), vec![])),
1264                    Box::new(Expr::BVar(1)),
1265                )),
1266            )),
1267            Box::new(Expr::App(
1268                Box::new(Expr::Const(Name::str("Stream"), vec![])),
1269                Box::new(Expr::BVar(1)),
1270            )),
1271        )),
1272    )
1273}
1274/// `Stream.fusion_law`: stream fusion correctness axiom.
1275/// Type: {α β γ : Type} → (f : β → γ) → (g : α → β) → s : Stream α →
1276///       Stream.map f (Stream.map g s) = Stream.map (f ∘ g) s
1277pub fn strm_ext_fusion_law_ty() -> Expr {
1278    let prop = Expr::Sort(Level::zero());
1279    let type1 = Expr::Sort(Level::succ(Level::zero()));
1280    Expr::Pi(
1281        BinderInfo::Implicit,
1282        Name::str("α"),
1283        Box::new(type1.clone()),
1284        Box::new(Expr::Pi(
1285            BinderInfo::Implicit,
1286            Name::str("β"),
1287            Box::new(type1.clone()),
1288            Box::new(Expr::Pi(
1289                BinderInfo::Implicit,
1290                Name::str("γ"),
1291                Box::new(type1.clone()),
1292                Box::new(Expr::Pi(
1293                    BinderInfo::Default,
1294                    Name::str("f"),
1295                    Box::new(Expr::Pi(
1296                        BinderInfo::Default,
1297                        Name::str("_"),
1298                        Box::new(Expr::BVar(1)),
1299                        Box::new(Expr::BVar(1)),
1300                    )),
1301                    Box::new(Expr::Pi(
1302                        BinderInfo::Default,
1303                        Name::str("g"),
1304                        Box::new(Expr::Pi(
1305                            BinderInfo::Default,
1306                            Name::str("_"),
1307                            Box::new(Expr::BVar(3)),
1308                            Box::new(Expr::BVar(3)),
1309                        )),
1310                        Box::new(Expr::Pi(
1311                            BinderInfo::Default,
1312                            Name::str("s"),
1313                            Box::new(Expr::App(
1314                                Box::new(Expr::Const(Name::str("Stream"), vec![])),
1315                                Box::new(Expr::BVar(4)),
1316                            )),
1317                            Box::new(prop),
1318                        )),
1319                    )),
1320                )),
1321            )),
1322        )),
1323    )
1324}
1325/// `Stream.BöhmTree`: Böhm tree as lazy normal form of a stream term.
1326/// Type: Type → Type
1327pub fn strm_ext_bohm_tree_ty() -> Expr {
1328    let type1 = Expr::Sort(Level::succ(Level::zero()));
1329    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1330    Expr::Pi(
1331        BinderInfo::Default,
1332        Name::str("α"),
1333        Box::new(type1),
1334        Box::new(type2),
1335    )
1336}
1337/// `Stream.corecursion_unique`: uniqueness of corecursive definitions.
1338/// Type: {α σ : Type} → (f g : σ → Stream α) → (∀ s, f s = g s) → Prop
1339pub fn strm_ext_corecursion_unique_ty() -> Expr {
1340    let type1 = Expr::Sort(Level::succ(Level::zero()));
1341    let prop = Expr::Sort(Level::zero());
1342    Expr::Pi(
1343        BinderInfo::Implicit,
1344        Name::str("α"),
1345        Box::new(type1.clone()),
1346        Box::new(Expr::Pi(
1347            BinderInfo::Implicit,
1348            Name::str("σ"),
1349            Box::new(type1.clone()),
1350            Box::new(Expr::Pi(
1351                BinderInfo::Default,
1352                Name::str("f"),
1353                Box::new(Expr::Pi(
1354                    BinderInfo::Default,
1355                    Name::str("_"),
1356                    Box::new(Expr::BVar(0)),
1357                    Box::new(Expr::App(
1358                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
1359                        Box::new(Expr::BVar(2)),
1360                    )),
1361                )),
1362                Box::new(Expr::Pi(
1363                    BinderInfo::Default,
1364                    Name::str("g"),
1365                    Box::new(Expr::Pi(
1366                        BinderInfo::Default,
1367                        Name::str("_"),
1368                        Box::new(Expr::BVar(1)),
1369                        Box::new(Expr::App(
1370                            Box::new(Expr::Const(Name::str("Stream"), vec![])),
1371                            Box::new(Expr::BVar(3)),
1372                        )),
1373                    )),
1374                    Box::new(prop),
1375                )),
1376            )),
1377        )),
1378    )
1379}
1380/// `Stream.automaton`: a stream automaton (coalgebra for Stream functor).
1381/// Type: {S α : Type} → (S → Prod α S) → S → Stream α
1382pub fn strm_ext_automaton_ty() -> Expr {
1383    let type1 = Expr::Sort(Level::succ(Level::zero()));
1384    Expr::Pi(
1385        BinderInfo::Implicit,
1386        Name::str("S"),
1387        Box::new(type1.clone()),
1388        Box::new(Expr::Pi(
1389            BinderInfo::Implicit,
1390            Name::str("α"),
1391            Box::new(type1.clone()),
1392            Box::new(Expr::Pi(
1393                BinderInfo::Default,
1394                Name::str("step"),
1395                Box::new(Expr::Pi(
1396                    BinderInfo::Default,
1397                    Name::str("_"),
1398                    Box::new(Expr::BVar(1)),
1399                    Box::new(Expr::App(
1400                        Box::new(Expr::App(
1401                            Box::new(Expr::Const(Name::str("Prod"), vec![])),
1402                            Box::new(Expr::BVar(1)),
1403                        )),
1404                        Box::new(Expr::BVar(2)),
1405                    )),
1406                )),
1407                Box::new(Expr::Pi(
1408                    BinderInfo::Default,
1409                    Name::str("s0"),
1410                    Box::new(Expr::BVar(2)),
1411                    Box::new(Expr::App(
1412                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
1413                        Box::new(Expr::BVar(2)),
1414                    )),
1415                )),
1416            )),
1417        )),
1418    )
1419}
1420/// `WeightedAutomaton.type`: weighted automaton over streams.
1421/// Type: Type → Type → Type → Type
1422pub fn strm_ext_weighted_automaton_ty() -> Expr {
1423    let type1 = Expr::Sort(Level::succ(Level::zero()));
1424    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
1425    Expr::Pi(
1426        BinderInfo::Default,
1427        Name::str("S"),
1428        Box::new(type1.clone()),
1429        Box::new(Expr::Pi(
1430            BinderInfo::Default,
1431            Name::str("I"),
1432            Box::new(type1.clone()),
1433            Box::new(Expr::Pi(
1434                BinderInfo::Default,
1435                Name::str("W"),
1436                Box::new(type1),
1437                Box::new(type2),
1438            )),
1439        )),
1440    )
1441}
1442/// `BloomFilter.type`: a streaming Bloom filter.
1443/// Type: Nat → Nat → Type
1444pub fn strm_ext_bloom_filter_ty() -> Expr {
1445    let type1 = Expr::Sort(Level::succ(Level::zero()));
1446    Expr::Pi(
1447        BinderInfo::Default,
1448        Name::str("m"),
1449        Box::new(Expr::Const(Name::str("Nat"), vec![])),
1450        Box::new(Expr::Pi(
1451            BinderInfo::Default,
1452            Name::str("k"),
1453            Box::new(Expr::Const(Name::str("Nat"), vec![])),
1454            Box::new(type1),
1455        )),
1456    )
1457}
1458/// `CountMinSketch.type`: a streaming count-min sketch.
1459/// Type: Nat → Nat → Type
1460pub fn strm_ext_count_min_sketch_ty() -> Expr {
1461    let type1 = Expr::Sort(Level::succ(Level::zero()));
1462    Expr::Pi(
1463        BinderInfo::Default,
1464        Name::str("d"),
1465        Box::new(Expr::Const(Name::str("Nat"), vec![])),
1466        Box::new(Expr::Pi(
1467            BinderInfo::Default,
1468            Name::str("w"),
1469            Box::new(Expr::Const(Name::str("Nat"), vec![])),
1470            Box::new(type1),
1471        )),
1472    )
1473}
1474/// `Stream.circular_prog`: circular programming / tie-the-knot combinator.
1475/// Type: {α β : Type} → ((Stream α → β) → Stream α → β) → Stream α → β
1476pub fn strm_ext_circular_prog_ty() -> Expr {
1477    let type1 = Expr::Sort(Level::succ(Level::zero()));
1478    Expr::Pi(
1479        BinderInfo::Implicit,
1480        Name::str("α"),
1481        Box::new(type1.clone()),
1482        Box::new(Expr::Pi(
1483            BinderInfo::Implicit,
1484            Name::str("β"),
1485            Box::new(type1.clone()),
1486            Box::new(Expr::Pi(
1487                BinderInfo::Default,
1488                Name::str("body"),
1489                Box::new(Expr::Pi(
1490                    BinderInfo::Default,
1491                    Name::str("_"),
1492                    Box::new(Expr::Pi(
1493                        BinderInfo::Default,
1494                        Name::str("_"),
1495                        Box::new(Expr::App(
1496                            Box::new(Expr::Const(Name::str("Stream"), vec![])),
1497                            Box::new(Expr::BVar(1)),
1498                        )),
1499                        Box::new(Expr::BVar(2)),
1500                    )),
1501                    Box::new(Expr::Pi(
1502                        BinderInfo::Default,
1503                        Name::str("_"),
1504                        Box::new(Expr::App(
1505                            Box::new(Expr::Const(Name::str("Stream"), vec![])),
1506                            Box::new(Expr::BVar(2)),
1507                        )),
1508                        Box::new(Expr::BVar(3)),
1509                    )),
1510                )),
1511                Box::new(Expr::Pi(
1512                    BinderInfo::Default,
1513                    Name::str("s"),
1514                    Box::new(Expr::App(
1515                        Box::new(Expr::Const(Name::str("Stream"), vec![])),
1516                        Box::new(Expr::BVar(2)),
1517                    )),
1518                    Box::new(Expr::BVar(3)),
1519                )),
1520            )),
1521        )),
1522    )
1523}
oxilean_std/stream/functions.rs

oxilean_std/stream/
functions.rs
