oxilean_codegen/coq_backend/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use std::collections::{HashMap, HashSet};
7
8/// Top-level Coq declaration.
9#[derive(Debug, Clone, PartialEq)]
10pub enum CoqDecl {
11    /// `Definition f (params) : T := body.`
12    Definition {
13        name: String,
14        params: Vec<(String, CoqTerm)>,
15        ty: Option<CoqTerm>,
16        body: CoqTerm,
17    },
18    /// `Theorem name (params) : T. Proof. ... Qed.`
19    Theorem {
20        name: String,
21        params: Vec<(String, CoqTerm)>,
22        ty: CoqTerm,
23        proof: CoqProof,
24    },
25    /// `Lemma name (params) : T. Proof. ... Qed.`
26    Lemma {
27        name: String,
28        params: Vec<(String, CoqTerm)>,
29        ty: CoqTerm,
30        proof: CoqProof,
31    },
32    /// `Axiom name : T.`
33    Axiom { name: String, ty: CoqTerm },
34    /// `Inductive name params : Sort := constructors.`
35    Inductive(CoqInductive),
36    /// `Fixpoint f params : T := body.` (possibly mutual)
37    Fixpoint(Vec<CoqFixPoint>),
38    /// `Record name params : Sort := { fields }.`
39    RecordDecl(CoqRecord),
40    /// `Class name params := { methods }.`
41    ClassDecl(CoqClass),
42    /// `Instance name : class := { methods }.`
43    Instance(CoqInstance),
44    /// `Require Import module.`
45    Require(String),
46    /// `Open Scope scope_name.`
47    OpenScope(String),
48    /// `Notation "..." := term.`
49    Notation(String, CoqTerm),
50    /// A raw comment line
51    Comment(String),
52    /// A raw verbatim declaration (fallback)
53    Raw(String),
54}
55impl CoqDecl {
56    /// Emit the declaration as a Coq source string.
57    pub fn emit(&self) -> String {
58        match self {
59            CoqDecl::Definition {
60                name,
61                params,
62                ty,
63                body,
64            } => {
65                let ps = if params.is_empty() {
66                    String::new()
67                } else {
68                    format!(" {}", emit_binders(params, 0))
69                };
70                let ty_ann = ty
71                    .as_ref()
72                    .map(|t| format!(" : {}", t.emit(0)))
73                    .unwrap_or_default();
74                format!("Definition {}{}{} := {}.", name, ps, ty_ann, body.emit(1))
75            }
76            CoqDecl::Theorem {
77                name,
78                params,
79                ty,
80                proof,
81            }
82            | CoqDecl::Lemma {
83                name,
84                params,
85                ty,
86                proof,
87            } => {
88                let kw = match self {
89                    CoqDecl::Theorem { .. } => "Theorem",
90                    _ => "Lemma",
91                };
92                let ps = if params.is_empty() {
93                    String::new()
94                } else {
95                    format!(" {}", emit_binders(params, 0))
96                };
97                format!("{} {}{} : {}.\n{}", kw, name, ps, ty.emit(0), proof.emit(0))
98            }
99            CoqDecl::Axiom { name, ty } => format!("Axiom {} : {}.", name, ty.emit(0)),
100            CoqDecl::Inductive(ind) => {
101                let ps = if ind.params.is_empty() {
102                    String::new()
103                } else {
104                    format!(" {}", emit_binders(&ind.params, 0))
105                };
106                let mut out = format!("Inductive {}{} : {} :=\n", ind.name, ps, ind.sort);
107                for ctor in &ind.constructors {
108                    out.push_str(&format!("  | {} : {}\n", ctor.name, ctor.ty.emit(1)));
109                }
110                out.push('.');
111                out
112            }
113            CoqDecl::Fixpoint(fps) => {
114                let mut parts = Vec::new();
115                for fp in fps {
116                    let params = emit_binders(&fp.params, 0);
117                    let ret = fp
118                        .return_type
119                        .as_ref()
120                        .map(|t| format!(" : {}", t.emit(0)))
121                        .unwrap_or_default();
122                    let struct_ann = fp
123                        .struct_arg
124                        .as_ref()
125                        .map(|s| format!(" {{struct {}}}", s))
126                        .unwrap_or_default();
127                    parts.push(format!(
128                        "{} {}{}{} :=\n  {}",
129                        fp.name,
130                        params,
131                        struct_ann,
132                        ret,
133                        fp.body.emit(1)
134                    ));
135                }
136                if parts.len() == 1 {
137                    format!("Fixpoint {}.", parts[0])
138                } else {
139                    let head = parts[0].clone();
140                    let rest = parts[1..].join("\nwith ");
141                    format!("Fixpoint {}\nwith {}.", head, rest)
142                }
143            }
144            CoqDecl::RecordDecl(rec) => {
145                let ps = if rec.params.is_empty() {
146                    String::new()
147                } else {
148                    format!(" {}", emit_binders(&rec.params, 0))
149                };
150                let ctor = rec
151                    .constructor
152                    .as_ref()
153                    .map(|c| format!(" {}", c))
154                    .unwrap_or_default();
155                let mut out = format!("Record {}{} : {} :={} {{\n", rec.name, ps, rec.sort, ctor);
156                for field in &rec.fields {
157                    out.push_str(&format!("  {} : {};\n", field.name, field.ty.emit(1)));
158                }
159                out.push_str("}.");
160                out
161            }
162            CoqDecl::ClassDecl(cls) => {
163                let ps = if cls.params.is_empty() {
164                    String::new()
165                } else {
166                    format!(" {}", emit_binders(&cls.params, 0))
167                };
168                let mut out = format!("Class {}{} := {{\n", cls.name, ps);
169                for m in &cls.methods {
170                    out.push_str(&format!("  {} : {};\n", m.name, m.ty.emit(1)));
171                }
172                out.push_str("}.");
173                out
174            }
175            CoqDecl::Instance(inst) => {
176                let mut out = format!("Instance {} : {} := {{\n", inst.name, inst.class.emit(0));
177                for (meth, body) in &inst.methods {
178                    out.push_str(&format!("  {} := {};\n", meth, body.emit(1)));
179                }
180                out.push_str("}.");
181                out
182            }
183            CoqDecl::Require(module) => format!("Require Import {}.", module),
184            CoqDecl::OpenScope(scope) => format!("Open Scope {}.", scope),
185            CoqDecl::Notation(notation, term) => {
186                format!("Notation \"{}\" := {}.", notation, term.emit(0))
187            }
188            CoqDecl::Comment(text) => format!("(* {} *)", text),
189            CoqDecl::Raw(s) => s.clone(),
190        }
191    }
192}
193/// Coq context (list of section vars + hypotheses)
194#[allow(dead_code)]
195#[derive(Debug, Default)]
196pub struct CoqContext {
197    pub vars: Vec<CoqSectionVar>,
198    pub hyps: Vec<CoqHypothesis>,
199}
200#[allow(dead_code)]
201impl CoqContext {
202    pub fn new() -> Self {
203        Self::default()
204    }
205    pub fn add_var(&mut self, v: CoqSectionVar) {
206        self.vars.push(v);
207    }
208    pub fn add_hyp(&mut self, h: CoqHypothesis) {
209        self.hyps.push(h);
210    }
211    pub fn emit(&self) -> String {
212        let mut out = String::new();
213        for v in &self.vars {
214            out.push_str(&format!("{}\n", v));
215        }
216        for h in &self.hyps {
217            out.push_str(&format!("{}\n", h));
218        }
219        out
220    }
221}
222/// A `Class` declaration (type class).
223#[derive(Debug, Clone, PartialEq)]
224pub struct CoqClass {
225    /// Class name
226    pub name: String,
227    /// Class parameters (including the carrier type)
228    pub params: Vec<(String, CoqTerm)>,
229    /// Methods
230    pub methods: Vec<CoqField>,
231}
232/// Coq import / require
233#[allow(dead_code)]
234#[derive(Debug, Clone)]
235pub enum CoqImport {
236    Require(Vec<String>),
237    RequireImport(Vec<String>),
238    RequireExport(Vec<String>),
239    Import(Vec<String>),
240    Open(String),
241}
242/// Coq attribute
243#[allow(dead_code)]
244#[derive(Debug, Clone)]
245pub enum CoqAttribute {
246    Global,
247    Local,
248    Export,
249    Transparent,
250    Opaque,
251    Polymorphic,
252    Monomorphic,
253    Program,
254    Equations,
255    Custom(String),
256}
257/// Coq solve_obligations shorthand
258#[allow(dead_code)]
259#[derive(Debug, Clone)]
260pub struct CoqSolveObligations {
261    pub tactic: Option<String>,
262}
263/// A Coq proof script: `Proof. ... Qed.` (or `Admitted.`)
264#[derive(Debug, Clone, PartialEq)]
265pub struct CoqProof {
266    /// Tactic steps
267    pub tactics: Vec<CoqTactic>,
268    /// Use `Admitted.` instead of `Qed.`
269    pub admitted: bool,
270}
271impl CoqProof {
272    /// Construct a simple proof from a slice of tactics.
273    pub fn new(tactics: Vec<CoqTactic>) -> Self {
274        Self {
275            tactics,
276            admitted: false,
277        }
278    }
279    /// Construct an admitted (placeholder) proof.
280    pub fn admitted() -> Self {
281        Self {
282            tactics: Vec::new(),
283            admitted: true,
284        }
285    }
286    /// Emit as a `Proof. ... Qed.` block.
287    pub fn emit(&self, indent: usize) -> String {
288        let mut out = "Proof.\n".to_string();
289        for tac in &self.tactics {
290            out.push_str(&format!("  {}.\n", tac.emit(indent + 1)));
291        }
292        if self.admitted {
293            out.push_str("Admitted.");
294        } else {
295            out.push_str("Qed.");
296        }
297        out
298    }
299}
300/// Coq Example definition
301#[allow(dead_code)]
302#[derive(Debug, Clone)]
303pub struct CoqExample {
304    pub name: String,
305    pub statement: String,
306    pub proof: CoqTacticBlock,
307}
308/// A complete Coq source file (`.v`).
309#[derive(Debug, Clone)]
310pub struct CoqModule {
311    /// Top-level module name (used as a comment / `Module` block if needed)
312    pub name: String,
313    /// `Require Import` directives emitted before declarations
314    pub requires: Vec<String>,
315    /// `Open Scope` directives emitted after requires
316    pub opens: Vec<String>,
317    /// Top-level declarations
318    pub declarations: Vec<CoqDecl>,
319}
320impl CoqModule {
321    /// Construct an empty module.
322    pub fn new(name: impl Into<String>) -> Self {
323        Self {
324            name: name.into(),
325            requires: Vec::new(),
326            opens: Vec::new(),
327            declarations: Vec::new(),
328        }
329    }
330    /// Add a `Require Import` directive.
331    pub fn require(&mut self, module: impl Into<String>) {
332        self.requires.push(module.into());
333    }
334    /// Add an `Open Scope` directive.
335    pub fn open_scope(&mut self, scope: impl Into<String>) {
336        self.opens.push(scope.into());
337    }
338    /// Add a declaration.
339    pub fn add(&mut self, decl: CoqDecl) {
340        self.declarations.push(decl);
341    }
342    /// Emit the full Coq source as a `String`.
343    pub fn emit(&self) -> String {
344        let mut out = format!("(* Generated by OxiLean: {} *)\n\n", self.name);
345        for req in &self.requires {
346            out.push_str(&format!("Require Import {}.\n", req));
347        }
348        if !self.requires.is_empty() {
349            out.push('\n');
350        }
351        for scope in &self.opens {
352            out.push_str(&format!("Open Scope {}.\n", scope));
353        }
354        if !self.opens.is_empty() {
355            out.push('\n');
356        }
357        for decl in &self.declarations {
358            out.push_str(&decl.emit());
359            out.push_str("\n\n");
360        }
361        out
362    }
363}
364/// Coq hint database
365#[allow(dead_code)]
366#[derive(Debug, Clone)]
367pub enum CoqHint {
368    Resolve(Vec<String>, Option<String>),
369    Rewrite(Vec<String>, Option<String>),
370    Unfold(Vec<String>, Option<String>),
371    Immediate(Vec<String>, Option<String>),
372    Constructors(Vec<String>, Option<String>),
373    Extern(u32, Option<String>, String),
374}
375/// Coq definition with let-binding
376#[allow(dead_code)]
377#[derive(Debug, Clone)]
378pub struct CoqLetDef {
379    pub name: String,
380    pub params: Vec<(String, Option<String>)>,
381    pub return_type: Option<String>,
382    pub body: String,
383    pub is_opaque: bool,
384}
385/// Coq backend feature flags
386#[allow(dead_code)]
387#[derive(Debug, Clone, Default)]
388pub struct CoqFeatureFlags {
389    pub use_ssreflect: bool,
390    pub use_mathcomp: bool,
391    pub use_equations: bool,
392    pub use_stdpp: bool,
393    pub use_iris: bool,
394}
395/// Coq hypothesis declaration
396#[allow(dead_code)]
397#[derive(Debug, Clone)]
398pub struct CoqHypothesis {
399    pub name: String,
400    pub hyp_type: String,
401}
402/// Coq extraction directive
403#[allow(dead_code)]
404#[derive(Debug, Clone)]
405pub enum CoqExtraction {
406    Language(String),
407    Constant(String, String),
408    Inductive(String, String),
409    Inline(Vec<String>),
410    NoInline(Vec<String>),
411    RecursiveExtraction(String),
412    Extraction(String, String),
413    ExtractionLibrary(String, String),
414}
415/// Coq obligating tactic
416#[allow(dead_code)]
417#[derive(Debug, Clone)]
418pub struct CoqObligation {
419    pub n: u32,
420    pub tactics: Vec<CoqTacticExt>,
421}
422/// Coq ltac definition
423#[allow(dead_code)]
424#[derive(Debug, Clone)]
425pub struct CoqLtacDef {
426    pub name: String,
427    pub params: Vec<String>,
428    pub body: String,
429    pub is_recursive: bool,
430}
431/// Coq instance definition
432#[allow(dead_code)]
433#[derive(Debug, Clone)]
434pub struct CoqInstanceDef {
435    pub name: Option<String>,
436    pub class: String,
437    pub args: Vec<String>,
438    pub methods: Vec<(String, String)>,
439}
440/// Coq source buffer
441#[allow(dead_code)]
442#[derive(Debug, Default)]
443pub struct CoqExtSourceBuffer {
444    pub sections: Vec<String>,
445    pub current: String,
446    pub indent: usize,
447}
448#[allow(dead_code)]
449impl CoqExtSourceBuffer {
450    pub fn new() -> Self {
451        Self::default()
452    }
453    pub fn write(&mut self, s: &str) {
454        let indent = " ".repeat(self.indent * 2);
455        for line in s.lines() {
456            self.current.push_str(&indent);
457            self.current.push_str(line);
458            self.current.push('\n');
459        }
460    }
461    pub fn write_raw(&mut self, s: &str) {
462        self.current.push_str(s);
463    }
464    pub fn push_indent(&mut self) {
465        self.indent += 1;
466    }
467    pub fn pop_indent(&mut self) {
468        if self.indent > 0 {
469            self.indent -= 1;
470        }
471    }
472    pub fn commit_section(&mut self) {
473        let sec = std::mem::take(&mut self.current);
474        if !sec.is_empty() {
475            self.sections.push(sec);
476        }
477    }
478    pub fn finish(mut self) -> String {
479        self.commit_section();
480        self.sections.join("\n")
481    }
482}
483/// A single branch inside a `match` expression.
484/// `| ctor arg1 arg2 => body`
485#[derive(Debug, Clone, PartialEq)]
486pub struct CoqBranch {
487    /// Constructor name (e.g. `"O"`, `"S"`, `"nil"`, `"cons"`)
488    pub constructor: String,
489    /// Bound variable names for constructor arguments
490    pub args: Vec<String>,
491    /// Right-hand side of the branch
492    pub body: CoqTerm,
493}
494/// Gallina term AST.
495#[derive(Debug, Clone, PartialEq)]
496pub enum CoqTerm {
497    /// Variable or qualified name: `nat`, `List.length`, `Nat.add`
498    Var(String),
499    /// Application: `f a b c`
500    App(Box<CoqTerm>, Vec<CoqTerm>),
501    /// Lambda abstraction: `fun (x : T) (y : U) => body`
502    Lambda(Vec<(String, CoqTerm)>, Box<CoqTerm>),
503    /// Universal quantifier: `forall (x : T), P x`
504    Forall(Vec<(String, CoqTerm)>, Box<CoqTerm>),
505    /// Non-dependent function type: `T -> U`
506    Prod(Box<CoqTerm>, Box<CoqTerm>),
507    /// Let binding: `let x [: T] := rhs in body`
508    Let(String, Option<Box<CoqTerm>>, Box<CoqTerm>, Box<CoqTerm>),
509    /// Pattern match: `match scrutinee [as name] with | ... end`
510    Match(Box<CoqTerm>, Option<String>, Vec<CoqBranch>),
511    /// (Mutual) fixpoint: `fix f (n : nat) ... := body`
512    Fix(Vec<CoqFixPoint>),
513    /// Universe sort: `Prop`, `Set`, `Type`
514    Sort(CoqSort),
515    /// Hole / unification variable: `_`
516    Hole,
517    /// Integer literal: `0`, `42`, `-1`
518    Num(i64),
519    /// String literal: `"hello"`
520    Str(String),
521    /// Coercion / type ascription: `(term : T)`
522    Cast(Box<CoqTerm>, Box<CoqTerm>),
523    /// Implicit argument: `@f` (explicit application)
524    Explicit(Box<CoqTerm>),
525    /// Tuple/pair: `(a, b)` (syntactic sugar for `pair a b`)
526    Tuple(Vec<CoqTerm>),
527    /// List literal: `[a; b; c]`
528    List(Vec<CoqTerm>),
529    /// If-then-else: `if b then t else f`
530    IfThenElse(Box<CoqTerm>, Box<CoqTerm>, Box<CoqTerm>),
531}
532impl CoqTerm {
533    /// Emit as a Gallina string with the given indentation.
534    pub fn emit(&self, indent: usize) -> String {
535        let pad = "  ".repeat(indent);
536        match self {
537            CoqTerm::Var(s) => s.clone(),
538            CoqTerm::Num(n) => n.to_string(),
539            CoqTerm::Str(s) => format!("\"{}\"", escape_coq_string(s)),
540            CoqTerm::Hole => "_".to_string(),
541            CoqTerm::Sort(s) => s.to_string(),
542            CoqTerm::App(func, args) => {
543                let f = func.emit_atom(indent);
544                let a: Vec<String> = args.iter().map(|a| a.emit_atom(indent)).collect();
545                format!("{} {}", f, a.join(" "))
546            }
547            CoqTerm::Lambda(binders, body) => {
548                let bs = emit_binders(binders, indent);
549                format!("fun {} =>\n{}  {}", bs, pad, body.emit(indent + 1))
550            }
551            CoqTerm::Forall(binders, body) => {
552                let bs = emit_binders(binders, indent);
553                format!("forall {}, {}", bs, body.emit(indent))
554            }
555            CoqTerm::Prod(dom, cod) => {
556                format!("{} -> {}", dom.emit_atom(indent), cod.emit(indent))
557            }
558            CoqTerm::Let(x, ty, rhs, body) => {
559                let ty_ann = ty
560                    .as_ref()
561                    .map(|t| format!(" : {}", t.emit(indent)))
562                    .unwrap_or_default();
563                format!(
564                    "let {}{} := {} in\n{}{}",
565                    x,
566                    ty_ann,
567                    rhs.emit(indent + 1),
568                    pad,
569                    body.emit(indent)
570                )
571            }
572            CoqTerm::Match(scrutinee, alias, branches) => {
573                let alias_str = alias
574                    .as_ref()
575                    .map(|a| format!(" as {}", a))
576                    .unwrap_or_default();
577                let mut out = format!("match {}{} with\n", scrutinee.emit(indent), alias_str);
578                for b in branches {
579                    let args = if b.args.is_empty() {
580                        String::new()
581                    } else {
582                        format!(" {}", b.args.join(" "))
583                    };
584                    out.push_str(&format!(
585                        "{}| {}{} => {}\n",
586                        pad,
587                        b.constructor,
588                        args,
589                        b.body.emit(indent + 1)
590                    ));
591                }
592                out.push_str(&format!("{}end", pad));
593                out
594            }
595            CoqTerm::Fix(fps) => {
596                let mut parts = Vec::new();
597                for fp in fps {
598                    let params = emit_binders(&fp.params, indent);
599                    let ret = fp
600                        .return_type
601                        .as_ref()
602                        .map(|t| format!(" : {}", t.emit(indent)))
603                        .unwrap_or_default();
604                    let struct_ann = fp
605                        .struct_arg
606                        .as_ref()
607                        .map(|s| format!(" {{struct {}}}", s))
608                        .unwrap_or_default();
609                    parts.push(format!(
610                        "{} {}{}{} :=\n{}  {}",
611                        fp.name,
612                        params,
613                        struct_ann,
614                        ret,
615                        pad,
616                        fp.body.emit(indent + 1)
617                    ));
618                }
619                format!("fix {}", parts.join("\nwith "))
620            }
621            CoqTerm::Cast(term, ty) => {
622                format!("({} : {})", term.emit(indent), ty.emit(indent))
623            }
624            CoqTerm::Explicit(term) => format!("@{}", term.emit(indent)),
625            CoqTerm::Tuple(elems) => {
626                let es: Vec<String> = elems.iter().map(|e| e.emit(indent)).collect();
627                format!("({})", es.join(", "))
628            }
629            CoqTerm::List(elems) => {
630                let es: Vec<String> = elems.iter().map(|e| e.emit(indent)).collect();
631                format!("[{}]", es.join("; "))
632            }
633            CoqTerm::IfThenElse(cond, then_, else_) => {
634                format!(
635                    "if {} then {} else {}",
636                    cond.emit(indent),
637                    then_.emit(indent),
638                    else_.emit(indent)
639                )
640            }
641        }
642    }
643    /// Emit as an atomic term (wrap compound terms in parens).
644    pub(super) fn emit_atom(&self, indent: usize) -> String {
645        match self {
646            CoqTerm::Var(_)
647            | CoqTerm::Num(_)
648            | CoqTerm::Str(_)
649            | CoqTerm::Hole
650            | CoqTerm::Sort(_)
651            | CoqTerm::Tuple(_)
652            | CoqTerm::List(_) => self.emit(indent),
653            _ => format!("({})", self.emit(indent)),
654        }
655    }
656}
657/// Coq section variable declaration
658#[allow(dead_code)]
659#[derive(Debug, Clone)]
660pub struct CoqSectionVar {
661    pub names: Vec<String>,
662    pub var_type: String,
663}
664/// An `Instance` declaration (type class instance).
665#[derive(Debug, Clone, PartialEq)]
666pub struct CoqInstance {
667    /// Instance name
668    pub name: String,
669    /// Class applied to concrete types
670    pub class: CoqTerm,
671    /// Method implementations: `method := body`
672    pub methods: Vec<(String, CoqTerm)>,
673}
674/// Coq tactic
675#[allow(dead_code)]
676#[derive(Debug, Clone)]
677pub enum CoqTacticExt {
678    Intro(Vec<String>),
679    Apply(String),
680    Exact(String),
681    Rewrite(bool, String),
682    Simpl,
683    Ring,
684    Omega,
685    Lia,
686    Lra,
687    Auto,
688    EAuto,
689    Tauto,
690    Constructor,
691    Split,
692    Left,
693    Right,
694    Exists(String),
695    Induction(String),
696    Destruct(String),
697    Inversion(String),
698    Reflexivity,
699    Symmetry,
700    Transitivity(String),
701    Unfold(Vec<String>),
702    Fold(Vec<String>),
703    Assumption,
704    Contradiction,
705    Exfalso,
706    Clear(Vec<String>),
707    Rename(String, String),
708    Trivial,
709    Discriminate,
710    Injection(String),
711    FApply(String),
712    Subst(Option<String>),
713    Custom(String),
714}
715/// Coq version target
716#[allow(dead_code)]
717#[derive(Debug, Clone, PartialEq, Eq)]
718pub enum CoqVersion {
719    V8_14,
720    V8_15,
721    V8_16,
722    V8_17,
723    V8_18,
724    V8_19,
725    V8_20,
726    Rocq0_1,
727    Latest,
728}
729/// Coq name scope
730#[allow(dead_code)]
731#[derive(Debug, Default)]
732pub struct CoqNameScope {
733    pub names: Vec<std::collections::HashMap<String, String>>,
734}
735#[allow(dead_code)]
736impl CoqNameScope {
737    pub fn new() -> Self {
738        let mut s = Self::default();
739        s.names.push(std::collections::HashMap::new());
740        s
741    }
742    pub fn push(&mut self) {
743        self.names.push(std::collections::HashMap::new());
744    }
745    pub fn pop(&mut self) {
746        if self.names.len() > 1 {
747            self.names.pop();
748        }
749    }
750    pub fn bind(&mut self, name: &str, coq_name: &str) {
751        if let Some(scope) = self.names.last_mut() {
752            scope.insert(name.to_string(), coq_name.to_string());
753        }
754    }
755    pub fn lookup(&self, name: &str) -> Option<&String> {
756        for scope in self.names.iter().rev() {
757            if let Some(v) = scope.get(name) {
758                return Some(v);
759            }
760        }
761        None
762    }
763}
764/// A single fixpoint function (inside `Fixpoint` or `fix`).
765#[derive(Debug, Clone, PartialEq)]
766pub struct CoqFixPoint {
767    /// Function name
768    pub name: String,
769    /// Parameter list: `(x : T)`
770    pub params: Vec<(String, CoqTerm)>,
771    /// Optional return type annotation
772    pub return_type: Option<CoqTerm>,
773    /// Structurally decreasing argument name (for `{struct arg}`)
774    pub struct_arg: Option<String>,
775    /// Function body
776    pub body: CoqTerm,
777}
778/// Coq emit stats
779#[allow(dead_code)]
780#[derive(Debug, Default, Clone)]
781pub struct CoqExtEmitStats {
782    pub theorems_emitted: usize,
783    pub definitions_emitted: usize,
784    pub lemmas_emitted: usize,
785    pub axioms_emitted: usize,
786    pub tactics_emitted: usize,
787}
788/// Coq eval command variants
789#[allow(dead_code)]
790#[derive(Debug, Clone)]
791pub enum CoqEvalCmd {
792    Compute(String),
793    Eval(String, String),
794    Check(String),
795    Print(String),
796    About(String),
797    SearchPattern(String),
798}
799/// Coq universe level
800#[allow(dead_code)]
801#[derive(Debug, Clone, PartialEq)]
802pub enum CoqUniverse {
803    Prop,
804    Set,
805    Type(Option<u32>),
806    SProp,
807}
808/// Top-level `Record` declaration.
809#[derive(Debug, Clone, PartialEq)]
810pub struct CoqRecord {
811    /// Record name
812    pub name: String,
813    /// Type parameters
814    pub params: Vec<(String, CoqTerm)>,
815    /// Sort of the record
816    pub sort: CoqSort,
817    /// Optional constructor name (defaults to `"Build_<name>"`)
818    pub constructor: Option<String>,
819    /// Fields
820    pub fields: Vec<CoqField>,
821}
822/// Coq profiler
823#[allow(dead_code)]
824#[derive(Debug, Default)]
825pub struct CoqExtProfiler {
826    pub timings: Vec<(String, u64)>,
827}
828#[allow(dead_code)]
829impl CoqExtProfiler {
830    pub fn new() -> Self {
831        Self::default()
832    }
833    pub fn record(&mut self, pass: &str, us: u64) {
834        self.timings.push((pass.to_string(), us));
835    }
836    pub fn total_us(&self) -> u64 {
837        self.timings.iter().map(|(_, t)| t).sum()
838    }
839}
840/// Coq class definition
841#[allow(dead_code)]
842#[derive(Debug, Clone)]
843pub struct CoqClassDef {
844    pub name: String,
845    pub params: Vec<(String, String)>,
846    pub methods: Vec<(String, String)>,
847}
848/// Coq module system
849#[allow(dead_code)]
850#[derive(Debug, Clone)]
851pub struct CoqModuleDef {
852    pub name: String,
853    pub items: Vec<String>,
854    pub is_section: bool,
855}
856/// Coq name mangler
857#[allow(dead_code)]
858#[derive(Debug, Default)]
859pub struct CoqNameMangler {
860    pub used: std::collections::HashSet<String>,
861    pub map: std::collections::HashMap<String, String>,
862}
863#[allow(dead_code)]
864impl CoqNameMangler {
865    pub fn new() -> Self {
866        Self::default()
867    }
868    pub fn mangle(&mut self, name: &str) -> String {
869        if let Some(m) = self.map.get(name) {
870            return m.clone();
871        }
872        let mangled: String = name
873            .chars()
874            .map(|c| {
875                if c.is_alphanumeric() || c == '_' || c == '\'' {
876                    c
877                } else {
878                    '_'
879                }
880            })
881            .collect();
882        let coq_reserved = [
883            "Definition",
884            "Theorem",
885            "Lemma",
886            "Proof",
887            "Qed",
888            "Admitted",
889            "Require",
890            "Import",
891            "Module",
892            "Section",
893            "End",
894            "Record",
895            "Inductive",
896            "CoInductive",
897            "Class",
898            "Instance",
899            "forall",
900            "exists",
901            "fun",
902            "match",
903            "with",
904            "end",
905            "in",
906            "let",
907            "fix",
908            "cofix",
909            "if",
910            "then",
911            "else",
912            "return",
913            "Type",
914            "Prop",
915            "Set",
916        ];
917        let mut candidate = if coq_reserved.contains(&mangled.as_str()) {
918            format!("ox_{}", mangled)
919        } else {
920            mangled.clone()
921        };
922        let base = candidate.clone();
923        let mut counter = 0;
924        while self.used.contains(&candidate) {
925            counter += 1;
926            candidate = format!("{}_{}", base, counter);
927        }
928        self.used.insert(candidate.clone());
929        self.map.insert(name.to_string(), candidate.clone());
930        candidate
931    }
932}
933/// Coq id generator
934#[allow(dead_code)]
935#[derive(Debug, Default)]
936pub struct CoqExtIdGen {
937    pub(super) counter: u64,
938    pub(super) prefix: String,
939}
940#[allow(dead_code)]
941impl CoqExtIdGen {
942    pub fn new(prefix: &str) -> Self {
943        Self {
944            counter: 0,
945            prefix: prefix.to_string(),
946        }
947    }
948    pub fn next(&mut self) -> String {
949        let id = self.counter;
950        self.counter += 1;
951        format!("{}_{}", self.prefix, id)
952    }
953}
954/// Coq proof term emitter (for extract-based proofs)
955#[allow(dead_code)]
956#[derive(Debug, Default)]
957pub struct CoqProofTermEmitter {
958    pub proof_terms: Vec<(String, String)>,
959}
960#[allow(dead_code)]
961impl CoqProofTermEmitter {
962    pub fn new() -> Self {
963        Self::default()
964    }
965    pub fn add(&mut self, name: &str, term: &str) {
966        self.proof_terms.push((name.to_string(), term.to_string()));
967    }
968    pub fn emit_all(&self) -> String {
969        let mut out = String::new();
970        for (n, t) in &self.proof_terms {
971            out.push_str(&format!("Definition {}_proof := {}.\n", n, t));
972        }
973        out
974    }
975}
976/// Coq notation definition
977#[allow(dead_code)]
978#[derive(Debug, Clone)]
979pub struct CoqNotation {
980    pub pattern: String,
981    pub body: String,
982    pub level: Option<u32>,
983    pub assoc: Option<String>,
984    pub scope: Option<String>,
985}
986/// A single constructor in an `Inductive` type.
987#[derive(Debug, Clone, PartialEq)]
988pub struct CoqConstructor {
989    /// Constructor name
990    pub name: String,
991    /// Constructor type (usually a chain of `forall` / `->`)
992    pub ty: CoqTerm,
993}
994/// Coq code statistics
995#[allow(dead_code)]
996#[derive(Debug, Default, Clone)]
997pub struct CoqCodeStats {
998    pub theorems: usize,
999    pub definitions: usize,
1000    pub lemmas: usize,
1001    pub axioms: usize,
1002    pub instances: usize,
1003    pub classes: usize,
1004    pub modules: usize,
1005    pub total_lines: usize,
1006}
1007/// Coq tactic block
1008#[allow(dead_code)]
1009#[derive(Debug, Default, Clone)]
1010pub struct CoqTacticBlock {
1011    pub tactics: Vec<CoqTacticExt>,
1012}
1013#[allow(dead_code)]
1014impl CoqTacticBlock {
1015    pub fn new() -> Self {
1016        Self::default()
1017    }
1018    pub fn add(&mut self, tac: CoqTacticExt) {
1019        self.tactics.push(tac);
1020    }
1021    pub fn emit(&self) -> String {
1022        let mut out = String::from("Proof.\n");
1023        for t in &self.tactics {
1024            out.push_str(&format!("  {}.\n", t));
1025        }
1026        out.push_str("Qed.\n");
1027        out
1028    }
1029    pub fn emit_admitted(&self) -> String {
1030        let mut out = String::from("Proof.\n");
1031        for t in &self.tactics {
1032            out.push_str(&format!("  {}.\n", t));
1033        }
1034        out.push_str("Admitted.\n");
1035        out
1036    }
1037}
1038/// Coq inductive definition (extended)
1039#[allow(dead_code)]
1040#[derive(Debug, Clone)]
1041pub struct CoqInductiveDef {
1042    pub name: String,
1043    pub params: Vec<(String, String)>,
1044    pub indices: Vec<(String, String)>,
1045    pub universe: CoqUniverse,
1046    pub constructors: Vec<(String, Vec<(String, String)>, String)>,
1047    pub is_coinductive: bool,
1048}
1049/// A single field in a `Record`.
1050#[derive(Debug, Clone, PartialEq)]
1051pub struct CoqField {
1052    /// Field name
1053    pub name: String,
1054    /// Field type
1055    pub ty: CoqTerm,
1056}
1057/// Coq diagnostics
1058#[allow(dead_code)]
1059#[derive(Debug, Clone, PartialEq, Eq)]
1060pub enum CoqDiagLevel {
1061    Info,
1062    Warning,
1063    Error,
1064}
1065#[allow(dead_code)]
1066#[derive(Debug, Default)]
1067pub struct CoqDiagSink {
1068    pub diags: Vec<CoqDiag>,
1069}
1070#[allow(dead_code)]
1071impl CoqDiagSink {
1072    pub fn new() -> Self {
1073        Self::default()
1074    }
1075    pub fn push(&mut self, level: CoqDiagLevel, msg: &str, item: Option<&str>) {
1076        self.diags.push(CoqDiag {
1077            level,
1078            message: msg.to_string(),
1079            item: item.map(|s| s.to_string()),
1080        });
1081    }
1082    pub fn has_errors(&self) -> bool {
1083        self.diags.iter().any(|d| d.level == CoqDiagLevel::Error)
1084    }
1085}
1086/// Coq module signature
1087#[allow(dead_code)]
1088#[derive(Debug, Clone, Default)]
1089pub struct CoqModuleSig {
1090    pub name: String,
1091    pub exports: Vec<String>,
1092}
1093#[allow(dead_code)]
1094impl CoqModuleSig {
1095    pub fn new(name: &str) -> Self {
1096        Self {
1097            name: name.to_string(),
1098            exports: Vec::new(),
1099        }
1100    }
1101    pub fn export(&mut self, item: &str) {
1102        self.exports.push(item.to_string());
1103    }
1104    pub fn emit(&self) -> String {
1105        format!(
1106            "Module Type {}.\n{}\nEnd {}.",
1107            self.name,
1108            self.exports
1109                .iter()
1110                .map(|e| format!("  Parameter {}.", e))
1111                .collect::<Vec<_>>()
1112                .join("\n"),
1113            self.name,
1114        )
1115    }
1116}
1117/// Top-level `Inductive` (or `Variant`) declaration.
1118#[derive(Debug, Clone, PartialEq)]
1119pub struct CoqInductive {
1120    /// Type name
1121    pub name: String,
1122    /// Universe parameters and type-level parameters: `(A : Set)`
1123    pub params: Vec<(String, CoqTerm)>,
1124    /// Sort of the inductive type itself
1125    pub sort: CoqSort,
1126    /// Constructors
1127    pub constructors: Vec<CoqConstructor>,
1128}
1129/// Coq extended backend config
1130#[allow(dead_code)]
1131#[derive(Debug, Clone)]
1132pub struct CoqExtConfig {
1133    pub emit_comments: bool,
1134    pub use_program: bool,
1135    pub use_equations: bool,
1136    pub universe_polymorphism: bool,
1137    pub default_db: String,
1138    pub emit_extracted: bool,
1139}
1140/// Ltac tactic AST.
1141#[derive(Debug, Clone, PartialEq)]
1142pub enum CoqTactic {
1143    /// `intro x y z`
1144    Intro(Vec<String>),
1145    /// `apply t`
1146    Apply(CoqTerm),
1147    /// `exact t`
1148    Exact(CoqTerm),
1149    /// `simpl` / `simpl in *`
1150    Simpl,
1151    /// `reflexivity`
1152    Reflexivity,
1153    /// `rewrite [<-] h`
1154    Rewrite(bool, CoqTerm),
1155    /// `induction x`
1156    Induction(String),
1157    /// `destruct x`
1158    Destruct(String),
1159    /// `auto`
1160    Auto,
1161    /// `omega`
1162    Omega,
1163    /// `lia` (Linear Integer Arithmetic)
1164    Lia,
1165    /// `ring`
1166    Ring,
1167    /// `unfold f g h`
1168    Unfold(Vec<String>),
1169    /// `compute`
1170    Compute,
1171    /// `assumption`
1172    Assumption,
1173    /// `tauto`
1174    Tauto,
1175    /// `decide`
1176    Decide,
1177    /// `trivial`
1178    Trivial,
1179    /// `split`
1180    Split,
1181    /// `left`
1182    Left,
1183    /// `right`
1184    Right,
1185    /// `exists witness`
1186    Exists(CoqTerm),
1187    /// `generalize t`
1188    Generalize(CoqTerm),
1189    /// `specialize (f a b)`
1190    Specialize(CoqTerm, Vec<CoqTerm>),
1191    /// `case t`
1192    Case(CoqTerm),
1193    /// `admit`
1194    Admit,
1195    /// Raw / custom tactic string
1196    Custom(String),
1197    /// Sequential composition: `t1. t2. t3.`
1198    Sequence(Vec<CoqTactic>),
1199    /// Then combinator: `t1; t2` (apply t2 to all subgoals of t1)
1200    Then(Box<CoqTactic>, Box<CoqTactic>),
1201}
1202impl CoqTactic {
1203    /// Emit as an Ltac string.
1204    pub fn emit(&self, indent: usize) -> String {
1205        let pad = "  ".repeat(indent);
1206        match self {
1207            CoqTactic::Intro(names) => {
1208                if names.is_empty() {
1209                    "intro".to_string()
1210                } else {
1211                    format!("intro {}", names.join(" "))
1212                }
1213            }
1214            CoqTactic::Apply(t) => format!("apply {}", t.emit(indent)),
1215            CoqTactic::Exact(t) => format!("exact {}", t.emit(indent)),
1216            CoqTactic::Simpl => "simpl".to_string(),
1217            CoqTactic::Reflexivity => "reflexivity".to_string(),
1218            CoqTactic::Rewrite(backward, t) => {
1219                if *backward {
1220                    format!("rewrite <- {}", t.emit(indent))
1221                } else {
1222                    format!("rewrite -> {}", t.emit(indent))
1223                }
1224            }
1225            CoqTactic::Induction(x) => format!("induction {}", x),
1226            CoqTactic::Destruct(x) => format!("destruct {}", x),
1227            CoqTactic::Auto => "auto".to_string(),
1228            CoqTactic::Omega => "omega".to_string(),
1229            CoqTactic::Lia => "lia".to_string(),
1230            CoqTactic::Ring => "ring".to_string(),
1231            CoqTactic::Unfold(names) => format!("unfold {}", names.join(", ")),
1232            CoqTactic::Compute => "compute".to_string(),
1233            CoqTactic::Assumption => "assumption".to_string(),
1234            CoqTactic::Tauto => "tauto".to_string(),
1235            CoqTactic::Decide => "decide".to_string(),
1236            CoqTactic::Trivial => "trivial".to_string(),
1237            CoqTactic::Split => "split".to_string(),
1238            CoqTactic::Left => "left".to_string(),
1239            CoqTactic::Right => "right".to_string(),
1240            CoqTactic::Exists(w) => format!("exists {}", w.emit(indent)),
1241            CoqTactic::Generalize(t) => format!("generalize {}", t.emit(indent)),
1242            CoqTactic::Specialize(f, args) => {
1243                let all: Vec<CoqTerm> = std::iter::once(f.clone())
1244                    .chain(args.iter().cloned())
1245                    .collect();
1246                let parts: Vec<String> = all.iter().map(|t| t.emit(indent)).collect();
1247                format!("specialize ({} {})", parts[0], parts[1..].join(" "))
1248            }
1249            CoqTactic::Case(t) => format!("case {}", t.emit(indent)),
1250            CoqTactic::Admit => "admit".to_string(),
1251            CoqTactic::Custom(s) => s.clone(),
1252            CoqTactic::Sequence(tactics) => tactics
1253                .iter()
1254                .map(|t| format!("{}{}.", pad, t.emit(indent)))
1255                .collect::<Vec<_>>()
1256                .join("\n"),
1257            CoqTactic::Then(t1, t2) => {
1258                format!("{}; {}", t1.emit(indent), t2.emit(indent))
1259            }
1260        }
1261    }
1262}
1263/// Coq program builder
1264#[allow(dead_code)]
1265#[derive(Debug, Default)]
1266pub struct CoqProgramBuilder {
1267    pub imports: Vec<CoqImport>,
1268    pub type_defs: Vec<String>,
1269    pub items: Vec<String>,
1270}
1271#[allow(dead_code)]
1272impl CoqProgramBuilder {
1273    pub fn new() -> Self {
1274        Self::default()
1275    }
1276    pub fn add_import(&mut self, import: CoqImport) {
1277        self.imports.push(import);
1278    }
1279    pub fn add_type_def(&mut self, td: &str) {
1280        self.type_defs.push(td.to_string());
1281    }
1282    pub fn add_item(&mut self, item: &str) {
1283        self.items.push(item.to_string());
1284    }
1285    pub fn build(&self) -> String {
1286        let mut out = String::new();
1287        for imp in &self.imports {
1288            out.push_str(&format!("{}\n", imp));
1289        }
1290        if !self.imports.is_empty() {
1291            out.push('\n');
1292        }
1293        for td in &self.type_defs {
1294            out.push_str(td);
1295            out.push('\n');
1296        }
1297        if !self.type_defs.is_empty() {
1298            out.push('\n');
1299        }
1300        for item in &self.items {
1301            out.push_str(item);
1302            out.push('\n');
1303        }
1304        out
1305    }
1306}
1307/// Coq record definition
1308#[allow(dead_code)]
1309#[derive(Debug, Clone)]
1310pub struct CoqRecordDef {
1311    pub name: String,
1312    pub params: Vec<(String, String)>,
1313    pub universe: CoqUniverse,
1314    pub constructor: Option<String>,
1315    pub fields: Vec<(String, String)>,
1316}
1317/// Universe sort in Coq's Calculus of Inductive Constructions.
1318#[derive(Debug, Clone, PartialEq, Eq)]
1319pub enum CoqSort {
1320    /// `Prop` — impredicative sort for logical propositions
1321    Prop,
1322    /// `Set` — predicative sort for computational data types
1323    Set,
1324    /// `Type` — universe-polymorphic sort; `Type(None)` = `Type`, `Type(Some(i))` = `Type@{i}`
1325    Type(Option<u32>),
1326}
1327#[allow(dead_code)]
1328#[derive(Debug, Clone)]
1329pub struct CoqDiag {
1330    pub level: CoqDiagLevel,
1331    pub message: String,
1332    pub item: Option<String>,
1333}
1334/// Coq tactic notation
1335#[allow(dead_code)]
1336#[derive(Debug, Clone)]
1337pub struct CoqTacticNotation {
1338    pub level: u32,
1339    pub pattern: Vec<String>,
1340    pub body: String,
1341}
1342/// Coq compute command
1343#[allow(dead_code)]
1344#[derive(Debug, Clone)]
1345pub struct CoqCompute {
1346    pub expr: String,
1347}
1348/// Coq pass builder (for integrating into pipeline)
1349#[allow(dead_code)]
1350#[derive(Debug, Default)]
1351pub struct CoqPassBuilder {
1352    pub config: CoqExtConfig,
1353    pub source: CoqExtSourceBuffer,
1354    pub stats: CoqExtEmitStats,
1355}
1356#[allow(dead_code)]
1357impl CoqPassBuilder {
1358    pub fn new() -> Self {
1359        Self::default()
1360    }
1361    pub fn with_config(mut self, cfg: CoqExtConfig) -> Self {
1362        self.config = cfg;
1363        self
1364    }
1365    pub fn finish(self) -> String {
1366        self.source.finish()
1367    }
1368    pub fn report(&self) -> String {
1369        format!("{}", self.stats)
1370    }
1371}
1372/// Coq universe polymorphism context
1373#[allow(dead_code)]
1374#[derive(Debug, Default, Clone)]
1375pub struct CoqUniverseCtx {
1376    pub levels: Vec<String>,
1377    pub constraints: Vec<(String, String, String)>,
1378}
1379#[allow(dead_code)]
1380impl CoqUniverseCtx {
1381    pub fn new() -> Self {
1382        Self::default()
1383    }
1384    pub fn add_level(&mut self, name: &str) {
1385        self.levels.push(name.to_string());
1386    }
1387    pub fn add_lt(&mut self, u: &str, v: &str) {
1388        self.constraints
1389            .push((u.to_string(), "<".to_string(), v.to_string()));
1390    }
1391    pub fn add_le(&mut self, u: &str, v: &str) {
1392        self.constraints
1393            .push((u.to_string(), "<=".to_string(), v.to_string()));
1394    }
1395    pub fn emit_poly_annotation(&self) -> String {
1396        if self.levels.is_empty() {
1397            return String::new();
1398        }
1399        format!("@{{{}}} ", self.levels.join(" "))
1400    }
1401}
1402/// Coq fixpoint definition
1403#[allow(dead_code)]
1404#[derive(Debug, Clone)]
1405pub struct CoqFixpointDef {
1406    pub name: String,
1407    pub params: Vec<(String, String)>,
1408    pub return_type: String,
1409    pub struct_arg: Option<String>,
1410    pub body: String,
1411}
1412/// Coq where-clause
1413#[allow(dead_code)]
1414#[derive(Debug, Clone)]
1415pub struct CoqWhere {
1416    pub vars: Vec<(String, String)>,
1417}
oxilean_codegen/coq_backend/types.rs

oxilean_codegen/coq_backend/
types.rs
