oxilean_codegen/coq_backend/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::types::{
6    CoqBranch, CoqClass, CoqConstructor, CoqDecl, CoqField, CoqFixPoint, CoqInductive, CoqInstance,
7    CoqModule, CoqProof, CoqRecord, CoqSort, CoqTactic, CoqTerm,
8};
9
10/// Emit a list of binders as `(x : T) (y : U)`.
11pub(super) fn emit_binders(binders: &[(String, CoqTerm)], indent: usize) -> String {
12    binders
13        .iter()
14        .map(|(x, ty)| format!("({} : {})", x, ty.emit(indent)))
15        .collect::<Vec<_>>()
16        .join(" ")
17}
18/// Escape special characters in a Coq string literal.
19pub(super) fn escape_coq_string(s: &str) -> String {
20    let mut out = String::with_capacity(s.len());
21    for c in s.chars() {
22        match c {
23            '"' => out.push_str("\"\""),
24            '\\' => out.push_str("\\\\"),
25            c => out.push(c),
26        }
27    }
28    out
29}
30/// Build `CoqTerm::Var`.
31pub fn var(name: impl Into<String>) -> CoqTerm {
32    CoqTerm::Var(name.into())
33}
34/// Build `CoqTerm::App`.
35pub fn app(func: CoqTerm, args: Vec<CoqTerm>) -> CoqTerm {
36    CoqTerm::App(Box::new(func), args)
37}
38/// Build a unary application: `f x`.
39pub fn app1(func: CoqTerm, arg: CoqTerm) -> CoqTerm {
40    CoqTerm::App(Box::new(func), vec![arg])
41}
42/// Build `CoqTerm::Forall`.
43pub fn forall(binders: Vec<(String, CoqTerm)>, body: CoqTerm) -> CoqTerm {
44    CoqTerm::Forall(binders, Box::new(body))
45}
46/// Build `CoqTerm::Prod` (non-dependent arrow).
47pub fn arrow(dom: CoqTerm, cod: CoqTerm) -> CoqTerm {
48    CoqTerm::Prod(Box::new(dom), Box::new(cod))
49}
50/// Build `CoqTerm::Lambda`.
51pub fn lambda(binders: Vec<(String, CoqTerm)>, body: CoqTerm) -> CoqTerm {
52    CoqTerm::Lambda(binders, Box::new(body))
53}
54#[cfg(test)]
55mod tests {
56    use super::*;
57    pub(super) fn nat() -> CoqTerm {
58        var("nat")
59    }
60    pub(super) fn bool_t() -> CoqTerm {
61        var("bool")
62    }
63    pub(super) fn prop() -> CoqTerm {
64        CoqTerm::Sort(CoqSort::Prop)
65    }
66    #[test]
67    pub(super) fn test_sort_prop() {
68        assert_eq!(CoqSort::Prop.to_string(), "Prop");
69    }
70    #[test]
71    pub(super) fn test_sort_set() {
72        assert_eq!(CoqSort::Set.to_string(), "Set");
73    }
74    #[test]
75    pub(super) fn test_sort_type_univ() {
76        assert_eq!(CoqSort::Type(None).to_string(), "Type");
77    }
78    #[test]
79    pub(super) fn test_sort_type_indexed() {
80        assert_eq!(CoqSort::Type(Some(2)).to_string(), "Type@{u2}");
81    }
82    #[test]
83    pub(super) fn test_var() {
84        assert_eq!(var("nat").emit(0), "nat");
85    }
86    #[test]
87    pub(super) fn test_num() {
88        assert_eq!(CoqTerm::Num(42).emit(0), "42");
89        assert_eq!(CoqTerm::Num(-1).emit(0), "-1");
90    }
91    #[test]
92    pub(super) fn test_str_literal() {
93        assert_eq!(CoqTerm::Str("hello".into()).emit(0), "\"hello\"");
94    }
95    #[test]
96    pub(super) fn test_str_escape() {
97        assert_eq!(CoqTerm::Str("say \"hi\"".into()).emit(0), r#""say ""hi""""#);
98    }
99    #[test]
100    pub(super) fn test_hole() {
101        assert_eq!(CoqTerm::Hole.emit(0), "_");
102    }
103    #[test]
104    pub(super) fn test_app_simple() {
105        let t = app(var("S"), vec![var("n")]);
106        assert_eq!(t.emit(0), "S n");
107    }
108    #[test]
109    pub(super) fn test_app_nested() {
110        let inner = app(var("plus"), vec![var("n"), var("m")]);
111        let outer = app(var("S"), vec![inner]);
112        assert_eq!(outer.emit(0), "S (plus n m)");
113    }
114    #[test]
115    pub(super) fn test_arrow_type() {
116        let t = arrow(nat(), nat());
117        assert_eq!(t.emit(0), "nat -> nat");
118    }
119    #[test]
120    pub(super) fn test_forall_type() {
121        let t = forall(
122            vec![("n".into(), nat()), ("m".into(), nat())],
123            app(
124                var("eq"),
125                vec![
126                    app(var("plus"), vec![var("n"), var("m")]),
127                    app(var("plus"), vec![var("m"), var("n")]),
128                ],
129            ),
130        );
131        let s = t.emit(0);
132        assert!(s.starts_with("forall (n : nat) (m : nat),"));
133    }
134    #[test]
135    pub(super) fn test_lambda() {
136        let t = lambda(vec![("n".into(), nat())], app(var("S"), vec![var("n")]));
137        let s = t.emit(0);
138        assert!(s.contains("fun (n : nat) =>"));
139        assert!(s.contains("S n"));
140    }
141    #[test]
142    pub(super) fn test_let_binding() {
143        let t = CoqTerm::Let(
144            "x".into(),
145            Some(Box::new(nat())),
146            Box::new(CoqTerm::Num(3)),
147            Box::new(app(var("S"), vec![var("x")])),
148        );
149        let s = t.emit(0);
150        assert!(s.contains("let x : nat := 3 in"));
151    }
152    #[test]
153    pub(super) fn test_tuple() {
154        let t = CoqTerm::Tuple(vec![CoqTerm::Num(1), CoqTerm::Num(2)]);
155        assert_eq!(t.emit(0), "(1, 2)");
156    }
157    #[test]
158    pub(super) fn test_list_literal() {
159        let t = CoqTerm::List(vec![CoqTerm::Num(1), CoqTerm::Num(2), CoqTerm::Num(3)]);
160        assert_eq!(t.emit(0), "[1; 2; 3]");
161    }
162    #[test]
163    pub(super) fn test_if_then_else() {
164        let t = CoqTerm::IfThenElse(
165            Box::new(var("b")),
166            Box::new(CoqTerm::Num(1)),
167            Box::new(CoqTerm::Num(0)),
168        );
169        assert_eq!(t.emit(0), "if b then 1 else 0");
170    }
171    #[test]
172    pub(super) fn test_match_expr() {
173        let t = CoqTerm::Match(
174            Box::new(var("n")),
175            None,
176            vec![
177                CoqBranch {
178                    constructor: "O".into(),
179                    args: vec![],
180                    body: CoqTerm::Num(0),
181                },
182                CoqBranch {
183                    constructor: "S".into(),
184                    args: vec!["n'".into()],
185                    body: app(var("S"), vec![app(var("S"), vec![var("n'")])]),
186                },
187            ],
188        );
189        let s = t.emit(0);
190        assert!(s.contains("| O => 0"));
191        assert!(s.contains("| S n' =>"));
192    }
193    #[test]
194    pub(super) fn test_tactic_intro() {
195        let t = CoqTactic::Intro(vec!["n".into(), "m".into()]);
196        assert_eq!(t.emit(0), "intro n m");
197    }
198    #[test]
199    pub(super) fn test_tactic_apply() {
200        let t = CoqTactic::Apply(var("plus_comm"));
201        assert_eq!(t.emit(0), "apply plus_comm");
202    }
203    #[test]
204    pub(super) fn test_tactic_rewrite_fwd() {
205        let t = CoqTactic::Rewrite(false, var("H"));
206        assert_eq!(t.emit(0), "rewrite -> H");
207    }
208    #[test]
209    pub(super) fn test_tactic_rewrite_bwd() {
210        let t = CoqTactic::Rewrite(true, var("H"));
211        assert_eq!(t.emit(0), "rewrite <- H");
212    }
213    #[test]
214    pub(super) fn test_tactic_induction() {
215        let t = CoqTactic::Induction("n".into());
216        assert_eq!(t.emit(0), "induction n");
217    }
218    #[test]
219    pub(super) fn test_tactic_then() {
220        let t = CoqTactic::Then(
221            Box::new(CoqTactic::Induction("n".into())),
222            Box::new(CoqTactic::Auto),
223        );
224        assert_eq!(t.emit(0), "induction n; auto");
225    }
226    #[test]
227    pub(super) fn test_tactic_exists() {
228        let t = CoqTactic::Exists(CoqTerm::Num(42));
229        assert_eq!(t.emit(0), "exists 42");
230    }
231    #[test]
232    pub(super) fn test_tactic_specialize() {
233        let t = CoqTactic::Specialize(var("H"), vec![var("n")]);
234        assert_eq!(t.emit(0), "specialize (H n)");
235    }
236    #[test]
237    pub(super) fn test_proof_reflexivity() {
238        let p = CoqProof::new(vec![CoqTactic::Reflexivity]);
239        let s = p.emit(0);
240        assert!(s.starts_with("Proof."));
241        assert!(s.contains("reflexivity."));
242        assert!(s.ends_with("Qed."));
243    }
244    #[test]
245    pub(super) fn test_proof_admitted() {
246        let p = CoqProof::admitted();
247        assert!(p.emit(0).ends_with("Admitted."));
248    }
249    #[test]
250    pub(super) fn test_decl_definition() {
251        let d = CoqDecl::Definition {
252            name: "double".into(),
253            params: vec![("n".into(), nat())],
254            ty: Some(nat()),
255            body: app(var("plus"), vec![var("n"), var("n")]),
256        };
257        let s = d.emit();
258        assert!(s.starts_with("Definition double"));
259        assert!(s.contains(":= plus n n."));
260    }
261    #[test]
262    pub(super) fn test_decl_axiom() {
263        let d = CoqDecl::Axiom {
264            name: "classic".into(),
265            ty: forall(
266                vec![("P".into(), prop())],
267                app(var("or"), vec![var("P"), app(var("not"), vec![var("P")])]),
268            ),
269        };
270        let s = d.emit();
271        assert!(s.starts_with("Axiom classic :"));
272    }
273    #[test]
274    pub(super) fn test_decl_inductive_nat() {
275        let d = CoqDecl::Inductive(CoqInductive {
276            name: "MyNat".into(),
277            params: vec![],
278            sort: CoqSort::Set,
279            constructors: vec![
280                CoqConstructor {
281                    name: "MyO".into(),
282                    ty: var("MyNat"),
283                },
284                CoqConstructor {
285                    name: "MyS".into(),
286                    ty: arrow(var("MyNat"), var("MyNat")),
287                },
288            ],
289        });
290        let s = d.emit();
291        assert!(s.contains("Inductive MyNat : Set :="));
292        assert!(s.contains("| MyO : MyNat"));
293        assert!(s.contains("| MyS : MyNat -> MyNat"));
294    }
295    #[test]
296    pub(super) fn test_decl_fixpoint() {
297        let d = CoqDecl::Fixpoint(vec![CoqFixPoint {
298            name: "add".into(),
299            params: vec![("n".into(), nat()), ("m".into(), nat())],
300            return_type: Some(nat()),
301            struct_arg: Some("n".into()),
302            body: CoqTerm::Match(
303                Box::new(var("n")),
304                None,
305                vec![
306                    CoqBranch {
307                        constructor: "O".into(),
308                        args: vec![],
309                        body: var("m"),
310                    },
311                    CoqBranch {
312                        constructor: "S".into(),
313                        args: vec!["n'".into()],
314                        body: app(var("S"), vec![app(var("add"), vec![var("n'"), var("m")])]),
315                    },
316                ],
317            ),
318        }]);
319        let s = d.emit();
320        assert!(s.starts_with("Fixpoint add"));
321        assert!(s.contains("{struct n}"));
322    }
323    #[test]
324    pub(super) fn test_decl_record() {
325        let d = CoqDecl::RecordDecl(CoqRecord {
326            name: "Point".into(),
327            params: vec![],
328            sort: CoqSort::Set,
329            constructor: Some("mkPoint".into()),
330            fields: vec![
331                CoqField {
332                    name: "x".into(),
333                    ty: var("R"),
334                },
335                CoqField {
336                    name: "y".into(),
337                    ty: var("R"),
338                },
339            ],
340        });
341        let s = d.emit();
342        assert!(s.contains("Record Point"));
343        assert!(s.contains("x : R;"));
344        assert!(s.contains("y : R;"));
345    }
346    #[test]
347    pub(super) fn test_decl_class() {
348        let d = CoqDecl::ClassDecl(CoqClass {
349            name: "Eq".into(),
350            params: vec![("A".into(), CoqTerm::Sort(CoqSort::Type(None)))],
351            methods: vec![CoqField {
352                name: "eqb".into(),
353                ty: arrow(var("A"), arrow(var("A"), bool_t())),
354            }],
355        });
356        let s = d.emit();
357        assert!(s.contains("Class Eq"));
358        assert!(s.contains("eqb : A -> A -> bool;"));
359    }
360    #[test]
361    pub(super) fn test_decl_instance() {
362        let d = CoqDecl::Instance(CoqInstance {
363            name: "NatEq".into(),
364            class: app1(var("Eq"), nat()),
365            methods: vec![("eqb".into(), var("Nat.eqb"))],
366        });
367        let s = d.emit();
368        assert!(s.contains("Instance NatEq : Eq nat"));
369        assert!(s.contains("eqb := Nat.eqb;"));
370    }
371    #[test]
372    pub(super) fn test_decl_theorem() {
373        let d = CoqDecl::Theorem {
374            name: "plus_O_n".into(),
375            params: vec![],
376            ty: forall(
377                vec![("n".into(), nat())],
378                app(
379                    var("eq"),
380                    vec![app(var("plus"), vec![CoqTerm::Num(0), var("n")]), var("n")],
381                ),
382            ),
383            proof: CoqProof::new(vec![
384                CoqTactic::Intro(vec!["n".into()]),
385                CoqTactic::Simpl,
386                CoqTactic::Reflexivity,
387            ]),
388        };
389        let s = d.emit();
390        assert!(s.starts_with("Theorem plus_O_n"));
391        assert!(s.contains("intro n."));
392        assert!(s.contains("Qed."));
393    }
394    #[test]
395    pub(super) fn test_module_emit() {
396        let mut m = CoqModule::new("Example");
397        m.require("Coq.Arith.Arith");
398        m.open_scope("nat_scope");
399        m.add(CoqDecl::Comment("simple definition".into()));
400        m.add(CoqDecl::Definition {
401            name: "one".into(),
402            params: vec![],
403            ty: Some(nat()),
404            body: app(var("S"), vec![var("O")]),
405        });
406        let s = m.emit();
407        assert!(s.contains("Require Import Coq.Arith.Arith."));
408        assert!(s.contains("Open Scope nat_scope."));
409        assert!(s.contains("(* simple definition *)"));
410        assert!(s.contains("Definition one"));
411    }
412    #[test]
413    pub(super) fn test_module_full_example() {
414        let mut m = CoqModule::new("ListExample");
415        m.require("Coq.Lists.List");
416        m.open_scope("list_scope");
417        m.add(CoqDecl::Fixpoint(vec![CoqFixPoint {
418            name: "my_length".into(),
419            params: vec![
420                ("A".into(), CoqTerm::Sort(CoqSort::Type(None))),
421                ("l".into(), app1(var("list"), var("A"))),
422            ],
423            return_type: Some(nat()),
424            struct_arg: Some("l".into()),
425            body: CoqTerm::Match(
426                Box::new(var("l")),
427                None,
428                vec![
429                    CoqBranch {
430                        constructor: "nil".into(),
431                        args: vec![],
432                        body: CoqTerm::Num(0),
433                    },
434                    CoqBranch {
435                        constructor: "cons".into(),
436                        args: vec!["_".into(), "t".into()],
437                        body: app(
438                            var("S"),
439                            vec![app(var("my_length"), vec![var("A"), var("t")])],
440                        ),
441                    },
442                ],
443            ),
444        }]));
445        let s = m.emit();
446        assert!(s.contains("Fixpoint my_length"));
447        assert!(s.contains("{struct l}"));
448        assert!(s.contains("| nil => 0"));
449    }
450}
451/// Coq final diagnostics helper
452#[allow(dead_code)]
453pub fn coq_emit_comment(text: &str) -> String {
454    format!("(* {} *)", text)
455}
456#[allow(dead_code)]
457pub fn coq_emit_section_separator(title: &str) -> String {
458    format!("(* ==================== {} ==================== *)", title)
459}
460#[allow(dead_code)]
461pub fn coq_emit_requires(mods: &[&str]) -> String {
462    format!("Require Import {}.", mods.join(" "))
463}
oxilean_codegen/coq_backend/functions.rs

oxilean_codegen/coq_backend/
functions.rs
