oxilean_codegen/idris_backend/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::types::{
6    IdrisBackend, IdrisConstructor, IdrisData, IdrisDecl, IdrisExpr, IdrisFunction, IdrisImport,
7    IdrisInterface, IdrisLiteral, IdrisModule, IdrisPattern, IdrisRecord, IdrisType, Visibility,
8};
9
10/// `ty_var(s)` — a type variable.
11pub fn ty_var(s: impl Into<String>) -> IdrisType {
12    IdrisType::Var(s.into())
13}
14/// `ty_data(name, args)` — a named data type application.
15pub fn ty_data(name: impl Into<String>, args: Vec<IdrisType>) -> IdrisType {
16    IdrisType::Data(name.into(), args)
17}
18/// `ty_fn(a, b)` — a function type `a -> b`.
19pub fn ty_fn(a: IdrisType, b: IdrisType) -> IdrisType {
20    IdrisType::Function(Box::new(a), Box::new(b))
21}
22/// `ty_pi(x, a, b)` — a dependent function type `(x : a) -> b`.
23pub fn ty_pi(x: impl Into<String>, a: IdrisType, b: IdrisType) -> IdrisType {
24    IdrisType::Pi(x.into(), Box::new(a), Box::new(b))
25}
26/// `expr_var(s)` — a variable expression.
27pub fn expr_var(s: impl Into<String>) -> IdrisExpr {
28    IdrisExpr::Var(s.into())
29}
30/// `expr_app(f, x)` — function application.
31pub fn expr_app(f: IdrisExpr, x: IdrisExpr) -> IdrisExpr {
32    IdrisExpr::App(Box::new(f), Box::new(x))
33}
34/// `expr_lam(params, body)` — lambda expression.
35pub fn expr_lam(params: Vec<String>, body: IdrisExpr) -> IdrisExpr {
36    IdrisExpr::Lam(params, Box::new(body))
37}
38/// `expr_int(n)` — integer literal.
39pub fn expr_int(n: i64) -> IdrisExpr {
40    IdrisExpr::Lit(IdrisLiteral::Int(n))
41}
42/// `expr_str(s)` — string literal.
43pub fn expr_str(s: impl Into<String>) -> IdrisExpr {
44    IdrisExpr::Lit(IdrisLiteral::Str(s.into()))
45}
46#[cfg(test)]
47mod tests {
48    use super::*;
49    #[test]
50    pub(super) fn test_type_display_basic() {
51        assert_eq!(format!("{}", IdrisType::Type), "Type");
52        assert_eq!(format!("{}", IdrisType::Nat), "Nat");
53        assert_eq!(format!("{}", IdrisType::Bool), "Bool");
54        assert_eq!(format!("{}", IdrisType::String), "String");
55        assert_eq!(format!("{}", IdrisType::Unit), "()");
56    }
57    #[test]
58    pub(super) fn test_type_display_function() {
59        let t = ty_fn(IdrisType::Nat, IdrisType::Bool);
60        assert_eq!(format!("{}", t), "Nat -> Bool");
61        let t2 = ty_fn(ty_fn(IdrisType::Nat, IdrisType::Nat), IdrisType::Bool);
62        let s = format!("{}", t2);
63        assert!(s.contains("->"), "got: {}", s);
64        assert!(s.starts_with('(') || s.contains("Nat -> Nat"), "got: {}", s);
65    }
66    #[test]
67    pub(super) fn test_type_display_list_vect() {
68        let lt = IdrisType::List(Box::new(IdrisType::Nat));
69        assert_eq!(format!("{}", lt), "List Nat");
70        let vt = IdrisType::Vect(
71            Box::new(IdrisExpr::Lit(IdrisLiteral::Nat(3))),
72            Box::new(IdrisType::Integer),
73        );
74        let s = format!("{}", vt);
75        assert!(s.starts_with("Vect"), "got: {}", s);
76        assert!(s.contains('3'), "got: {}", s);
77    }
78    #[test]
79    pub(super) fn test_type_display_pi() {
80        let t = ty_pi(
81            "n",
82            IdrisType::Nat,
83            ty_data("Vec", vec![ty_var("n"), IdrisType::Integer]),
84        );
85        let s = format!("{}", t);
86        assert!(s.contains("(n : Nat)"), "got: {}", s);
87        assert!(s.contains("->"), "got: {}", s);
88    }
89    #[test]
90    pub(super) fn test_expr_basic() {
91        assert_eq!(format!("{}", expr_var("x")), "x");
92        assert_eq!(format!("{}", expr_int(42)), "42");
93        assert_eq!(format!("{}", expr_str("hello")), "\"hello\"");
94        assert_eq!(format!("{}", IdrisExpr::Refl), "Refl");
95        assert_eq!(format!("{}", IdrisExpr::Hole("h".into())), "?h");
96    }
97    #[test]
98    pub(super) fn test_expr_app_lam() {
99        let app = expr_app(expr_var("succ"), expr_int(0));
100        assert_eq!(format!("{}", app), "succ 0");
101        let lam = expr_lam(
102            vec!["x".into(), "y".into()],
103            expr_app(expr_var("add"), expr_var("x")),
104        );
105        let s = format!("{}", lam);
106        assert!(s.starts_with('\\'), "got: {}", s);
107        assert!(s.contains("=>"), "got: {}", s);
108    }
109    #[test]
110    pub(super) fn test_expr_case_of() {
111        let scrutinee = expr_var("n");
112        let alts = vec![
113            (IdrisPattern::Con("Z".into(), vec![]), expr_int(0)),
114            (
115                IdrisPattern::Con("S".into(), vec![IdrisPattern::Var("k".into())]),
116                expr_var("k"),
117            ),
118        ];
119        let ce = IdrisExpr::CaseOf(Box::new(scrutinee), alts);
120        let s = format!("{}", ce);
121        assert!(s.contains("case n of"), "got: {}", s);
122        assert!(s.contains("Z"), "got: {}", s);
123        assert!(s.contains("(S k)"), "got: {}", s);
124    }
125    #[test]
126    pub(super) fn test_function_emit_simple() {
127        let f = IdrisFunction::new(
128            "double",
129            ty_fn(IdrisType::Nat, IdrisType::Nat),
130            expr_app(expr_app(expr_var("(*"), expr_int(2)), expr_var("n")),
131        );
132        let s = f.emit(0);
133        assert!(s.contains("double : Nat -> Nat"), "got: {}", s);
134        assert!(s.contains("double ="), "got: {}", s);
135    }
136    #[test]
137    pub(super) fn test_function_emit_clauses() {
138        let f = IdrisFunction::with_clauses(
139            "isZero",
140            ty_fn(IdrisType::Nat, IdrisType::Bool),
141            vec![
142                (
143                    vec![IdrisPattern::Con("Z".into(), vec![])],
144                    IdrisExpr::Lit(IdrisLiteral::True),
145                ),
146                (
147                    vec![IdrisPattern::Con("S".into(), vec![IdrisPattern::Wildcard])],
148                    IdrisExpr::Lit(IdrisLiteral::False),
149                ),
150            ],
151        );
152        let s = f.emit(0);
153        assert!(s.contains("isZero : Nat -> Bool"), "got: {}", s);
154        assert!(s.contains("isZero Z = True"), "got: {}", s);
155        assert!(s.contains("isZero (S _) = False"), "got: {}", s);
156    }
157    #[test]
158    pub(super) fn test_data_emit() {
159        let d = IdrisData {
160            name: "MyNat".into(),
161            params: vec![],
162            kind: IdrisType::Type,
163            constructors: vec![
164                IdrisConstructor {
165                    name: "MZ".into(),
166                    ty: ty_data("MyNat", vec![]),
167                    doc: None,
168                },
169                IdrisConstructor {
170                    name: "MS".into(),
171                    ty: ty_fn(ty_data("MyNat", vec![]), ty_data("MyNat", vec![])),
172                    doc: None,
173                },
174            ],
175            visibility: Visibility::PublicExport,
176            doc: None,
177        };
178        let s = d.emit(0);
179        assert!(
180            s.contains("public export data MyNat : Type where"),
181            "got: {}",
182            s
183        );
184        assert!(s.contains("MZ : MyNat"), "got: {}", s);
185        assert!(s.contains("MS : MyNat -> MyNat"), "got: {}", s);
186    }
187    #[test]
188    pub(super) fn test_record_emit() {
189        let r = IdrisRecord {
190            name: "Point".into(),
191            params: vec![("a".into(), IdrisType::Type)],
192            kind: IdrisType::Type,
193            constructor: "MkPoint".into(),
194            fields: vec![("x".into(), ty_var("a")), ("y".into(), ty_var("a"))],
195            visibility: Visibility::Export,
196            doc: Some("A 2D point".into()),
197        };
198        let s = r.emit(0);
199        assert!(s.contains("||| A 2D point"), "got: {}", s);
200        assert!(
201            s.contains("export record Point (a : Type) : Type where"),
202            "got: {}",
203            s
204        );
205        assert!(s.contains("constructor MkPoint"), "got: {}", s);
206        assert!(s.contains("x : a"), "got: {}", s);
207        assert!(s.contains("y : a"), "got: {}", s);
208    }
209    #[test]
210    pub(super) fn test_interface_emit() {
211        let iface = IdrisInterface {
212            name: "Container".into(),
213            constraints: vec![],
214            params: vec![("f".into(), ty_fn(IdrisType::Type, IdrisType::Type))],
215            methods: vec![
216                ("empty".into(), ty_data("f", vec![ty_var("a")])),
217                (
218                    "insert".into(),
219                    ty_fn(
220                        ty_var("a"),
221                        ty_fn(
222                            ty_data("f", vec![ty_var("a")]),
223                            ty_data("f", vec![ty_var("a")]),
224                        ),
225                    ),
226                ),
227            ],
228            defaults: vec![],
229            visibility: Visibility::PublicExport,
230            doc: None,
231        };
232        let s = iface.emit(0);
233        assert!(
234            s.contains("public export interface Container"),
235            "got: {}",
236            s
237        );
238        assert!(s.contains("empty :"), "got: {}", s);
239        assert!(s.contains("insert :"), "got: {}", s);
240    }
241    #[test]
242    pub(super) fn test_module_emit() {
243        let backend = IdrisBackend::new();
244        let mut m = IdrisModule::new(vec!["Data".into(), "MyVec".into()]);
245        m.import(IdrisImport::new(vec!["Data".into(), "Nat".into()]));
246        m.import(IdrisImport::public_import(vec![
247            "Data".into(),
248            "List".into(),
249        ]));
250        m.add(IdrisDecl::Data(IdrisData {
251            name: "Vec".into(),
252            params: vec![("n".into(), IdrisType::Nat), ("a".into(), IdrisType::Type)],
253            kind: IdrisType::Type,
254            constructors: vec![
255                IdrisConstructor {
256                    name: "Nil".into(),
257                    ty: ty_data("Vec", vec![ty_data("Z", vec![]), ty_var("a")]),
258                    doc: None,
259                },
260                IdrisConstructor {
261                    name: "Cons".into(),
262                    ty: ty_fn(
263                        ty_var("a"),
264                        ty_fn(
265                            ty_data("Vec", vec![ty_var("n"), ty_var("a")]),
266                            ty_data("Vec", vec![ty_data("S", vec![ty_var("n")]), ty_var("a")]),
267                        ),
268                    ),
269                    doc: None,
270                },
271            ],
272            visibility: Visibility::PublicExport,
273            doc: Some("Length-indexed vector".into()),
274        }));
275        let s = backend.emit_module(&m);
276        assert!(s.contains("module Data.MyVec"), "got: {}", s);
277        assert!(s.contains("import Data.Nat"), "got: {}", s);
278        assert!(s.contains("public import Data.List"), "got: {}", s);
279        assert!(s.contains("||| Length-indexed vector"), "got: {}", s);
280        assert!(s.contains("public export data Vec"), "got: {}", s);
281        assert!(s.contains("Nil :"), "got: {}", s);
282        assert!(s.contains("Cons :"), "got: {}", s);
283    }
284    #[test]
285    pub(super) fn test_namespace_and_mutual_emit() {
286        let backend = IdrisBackend::proof_mode();
287        let mut m = IdrisModule::new(vec!["Proof".into(), "Even".into()]);
288        let even_decl = IdrisDecl::Mutual(vec![
289            IdrisDecl::Func(IdrisFunction::with_clauses(
290                "isEven",
291                ty_fn(IdrisType::Nat, IdrisType::Bool),
292                vec![
293                    (
294                        vec![IdrisPattern::Con("Z".into(), vec![])],
295                        IdrisExpr::Lit(IdrisLiteral::True),
296                    ),
297                    (
298                        vec![IdrisPattern::Con(
299                            "S".into(),
300                            vec![IdrisPattern::Var("n".into())],
301                        )],
302                        expr_app(expr_var("isOdd"), expr_var("n")),
303                    ),
304                ],
305            )),
306            IdrisDecl::Func(IdrisFunction::with_clauses(
307                "isOdd",
308                ty_fn(IdrisType::Nat, IdrisType::Bool),
309                vec![
310                    (
311                        vec![IdrisPattern::Con("Z".into(), vec![])],
312                        IdrisExpr::Lit(IdrisLiteral::False),
313                    ),
314                    (
315                        vec![IdrisPattern::Con(
316                            "S".into(),
317                            vec![IdrisPattern::Var("n".into())],
318                        )],
319                        expr_app(expr_var("isEven"), expr_var("n")),
320                    ),
321                ],
322            )),
323        ]);
324        m.add(even_decl);
325        let s = backend.emit_module(&m);
326        assert!(s.starts_with("-- AUTO-GENERATED"), "got: {}", s);
327        assert!(s.contains("%default total"), "got: {}", s);
328        assert!(s.contains("module Proof.Even"), "got: {}", s);
329        assert!(s.contains("mutual"), "got: {}", s);
330        assert!(s.contains("isEven"), "got: {}", s);
331        assert!(s.contains("isOdd"), "got: {}", s);
332    }
333}
oxilean_codegen/idris_backend/functions.rs

oxilean_codegen/idris_backend/
functions.rs
