oxilean_codegen/ir_serialize/
types.rs

1//! Types for the LCNF IR serialization module.
2
3use std::collections::HashMap;
4
5/// A fully serialized Oxilean LCNF module ready for storage or transmission.
6#[allow(dead_code)]
7#[derive(Debug, Clone, PartialEq, Eq)]
8pub struct SerializedIr {
9    /// Format version used when this snapshot was written.
10    pub version: u32,
11    /// Fully-qualified name of the module.
12    pub module_name: String,
13    /// Every declaration exported by the module.
14    pub declarations: Vec<SerialDecl>,
15    /// Arbitrary key-value metadata (e.g. compiler flags, timestamps).
16    pub metadata: HashMap<String, String>,
17}
18
19/// A single serialized declaration inside a [`SerializedIr`] module.
20#[allow(dead_code)]
21#[derive(Debug, Clone, PartialEq, Eq)]
22pub struct SerialDecl {
23    /// The fully-qualified name of the declaration.
24    pub name: String,
25    /// The flavour of this declaration.
26    pub kind: DeclKind,
27    /// The type signature as a human-readable string.
28    pub type_: String,
29    /// The body (term) as a human-readable string, if present.
30    pub body: Option<String>,
31    /// Formal parameter names in order.
32    pub params: Vec<String>,
33}
34
35/// Possible kinds of LCNF declarations.
36#[allow(dead_code)]
37#[derive(Debug, Clone, PartialEq, Eq)]
38pub enum DeclKind {
39    /// An ordinary definition (`def`).
40    Def,
41    /// A proved theorem (`theorem`).
42    Theorem,
43    /// An axiom (unproved assumption).
44    Axiom,
45    /// An inductive type declaration.
46    Inductive,
47    /// A constructor of an inductive type.
48    Constructor,
49    /// A recursor / eliminator for an inductive type.
50    Recursor,
51}
52
53impl std::fmt::Display for DeclKind {
54    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
55        let s = match self {
56            DeclKind::Def => "def",
57            DeclKind::Theorem => "theorem",
58            DeclKind::Axiom => "axiom",
59            DeclKind::Inductive => "inductive",
60            DeclKind::Constructor => "constructor",
61            DeclKind::Recursor => "recursor",
62        };
63        f.write_str(s)
64    }
65}
66
67/// The serialization format to use when writing an IR snapshot.
68#[allow(dead_code)]
69#[derive(Debug, Clone, PartialEq, Eq)]
70pub enum IrFormat {
71    /// Human-readable plain-text format.
72    Text,
73    /// A compact binary encoding (length-prefixed fields).
74    Binary,
75    /// JSON encoding (UTF-8).
76    Json,
77}
78
79/// Configuration for the IR serializer.
80#[allow(dead_code)]
81#[derive(Debug, Clone)]
82pub struct IrSerializeConfig {
83    /// Which wire format to emit.
84    pub format: IrFormat,
85    /// Whether to pretty-print (indent) the output when supported.
86    pub pretty: bool,
87    /// Include type signatures in the output.
88    pub include_types: bool,
89    /// Include proof bodies in the output.
90    pub include_proofs: bool,
91}
92
93impl Default for IrSerializeConfig {
94    fn default() -> Self {
95        IrSerializeConfig {
96            format: IrFormat::Text,
97            pretty: true,
98            include_types: true,
99            include_proofs: true,
100        }
101    }
102}
103
104/// The result of attempting to deserialize an IR snapshot.
105#[allow(dead_code)]
106#[derive(Debug, Clone, PartialEq, Eq)]
107pub enum IrDeserializeResult {
108    /// Deserialization succeeded.
109    Ok(SerializedIr),
110    /// The snapshot was written with a different format version.
111    VersionMismatch {
112        /// The version the deserializer expects.
113        expected: u32,
114        /// The version found in the data.
115        found: u32,
116    },
117    /// The input could not be parsed.
118    ParseError(String),
119    /// The requested format is not supported by this deserializer.
120    Unsupported(String),
121}
oxilean_codegen/ir_serialize/types.rs

oxilean_codegen/ir_serialize/
types.rs
