oak-coq 0.0.11

Coq theorem prover language parser with support for dependent types and formal verification.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110

#![doc = include_str!("readme.md")]
use oak_core::Range;

/// Root node of the Coq AST (Abstract Syntax Tree).
///
/// This structure represents the top-level node of a Coq document,
/// containing a sequence of vernacular statements.
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, PartialEq, Clone)]
pub struct CoqRoot {
    /// A vector of vernacular statements that make up the Coq document.
    pub vernaculars: Vec<Vernacular>,
}

/// Represents a vernacular statement in Coq.
///
/// Vernaculars are top-level commands in Coq, such as definitions,
/// theorems, inductive types, etc.
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, PartialEq, Clone)]
pub enum Vernacular {
    /// A definition statement with a name, body, and source span.
    Definition {
        /// The name of the defined term.
        name: String,
        /// The body of the definition.
        body: String,
        /// The source span of the definition.
        #[cfg_attr(feature = "serde", serde(with = "oak_core::serde_range"))]
        span: Range<usize>,
    },
    /// A theorem statement with a name, statement, proof, and source span.
    Theorem {
        /// The name of the theorem.
        name: String,
        /// The statement of the theorem.
        statement: String,
        /// The proof of the theorem.
        proof: String,
        /// The source span of the theorem.
        #[cfg_attr(feature = "serde", serde(with = "oak_core::serde_range"))]
        span: Range<usize>,
    },
    /// An inductive type definition with a name, constructors, and source span.
    Inductive {
        /// The name of the inductive type.
        name: String,
        /// The constructors of the inductive type.
        constructors: Vec<String>,
        /// The source span of the inductive type definition.
        #[cfg_attr(feature = "serde", serde(with = "oak_core::serde_range"))]
        span: Range<usize>,
    },
    /// A fixpoint (recursive function) definition with a name, body, and source span.
    Fixpoint {
        /// The name of the fixpoint.
        name: String,
        /// The body of the fixpoint.
        body: String,
        /// The source span of the fixpoint definition.
        #[cfg_attr(feature = "serde", serde(with = "oak_core::serde_range"))]
        span: Range<usize>,
    },
    /// A Check command with a term and source span.
    Check {
        /// The term to check.
        term: String,
        /// The source span of the Check command.
        #[cfg_attr(feature = "serde", serde(with = "oak_core::serde_range"))]
        span: Range<usize>,
    },
    /// A Print command with a name and source span.
    Print {
        /// The name to print.
        name: String,
        /// The source span of the Print command.
        #[cfg_attr(feature = "serde", serde(with = "oak_core::serde_range"))]
        span: Range<usize>,
    },
}

impl CoqRoot {
    /// Creates a new empty CoqRoot.
    ///
    /// # Returns
    ///
    /// A new CoqRoot with no vernacular statements.
    pub fn new() -> Self {
        Self { vernaculars: Vec::new() }
    }

    /// Creates a new CoqRoot with the given vernacular statements.
    ///
    /// # Arguments
    ///
    /// * `vernaculars` - A vector of vernacular statements.
    ///
    /// # Returns
    ///
    /// A new CoqRoot containing the provided vernacular statements.
    pub fn with_vernaculars(vernaculars: Vec<Vernacular>) -> Self {
        Self { vernaculars }
    }
}

impl Default for CoqRoot {
    fn default() -> Self {
        Self::new()
    }
}