logicaffeine-kernel 0.9.16

Pure Calculus of Constructions type theory - NO LEXICON
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

//! Error types for the Vernacular interface.

use crate::KernelError;
use std::fmt;

/// Errors that can occur in the interface layer.
#[derive(Debug)]
pub enum InterfaceError {
    /// Parse error in command or term syntax.
    Parse(ParseError),

    /// Error from the kernel (type checking, etc.)
    Kernel(KernelError),
}

/// Parse errors for the Vernacular.
#[derive(Debug, Clone)]
pub enum ParseError {
    /// Unexpected end of input.
    UnexpectedEof,

    /// Unknown command keyword.
    UnknownCommand(String),

    /// Expected a specific token.
    Expected { expected: String, found: String },

    /// Invalid identifier.
    InvalidIdent(String),

    /// Invalid number literal.
    InvalidNumber(String),

    /// Missing required component.
    Missing(String),

    // ============================================================
    // Literate Syntax Errors
    // ============================================================

    /// Missing "is either" clause in inductive definition.
    MissingEitherClause,

    /// Missing variant name in inductive definition.
    MissingVariantName,

    /// Invalid Consider/When/Yield syntax.
    InvalidConsiderSyntax(String),

    /// Missing Yield in function body.
    MissingYield,

    /// Missing When clause in Consider block.
    MissingWhenClause,

    /// Unclosed Consider block.
    UnclosedConsiderBlock,
}

impl fmt::Display for InterfaceError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            InterfaceError::Parse(e) => write!(f, "Parse error: {}", e),
            InterfaceError::Kernel(e) => write!(f, "Kernel error: {}", e),
        }
    }
}

impl fmt::Display for ParseError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            ParseError::UnexpectedEof => write!(f, "Unexpected end of input"),
            ParseError::UnknownCommand(cmd) => write!(f, "Unknown command: {}", cmd),
            ParseError::Expected { expected, found } => {
                write!(f, "Expected {}, found {}", expected, found)
            }
            ParseError::InvalidIdent(s) => write!(f, "Invalid identifier: {}", s),
            ParseError::InvalidNumber(s) => write!(f, "Invalid number literal: {}", s),
            ParseError::Missing(what) => write!(f, "Missing {}", what),
            // Literate syntax errors
            ParseError::MissingEitherClause => write!(f, "Missing 'is either' clause in type definition"),
            ParseError::MissingVariantName => write!(f, "Missing variant name in type definition"),
            ParseError::InvalidConsiderSyntax(msg) => write!(f, "Invalid Consider syntax: {}", msg),
            ParseError::MissingYield => write!(f, "Missing 'Yield' in function body"),
            ParseError::MissingWhenClause => write!(f, "Missing 'When' clause in Consider block"),
            ParseError::UnclosedConsiderBlock => write!(f, "Unclosed Consider block"),
        }
    }
}

impl std::error::Error for InterfaceError {}
impl std::error::Error for ParseError {}

impl From<ParseError> for InterfaceError {
    fn from(e: ParseError) -> Self {
        InterfaceError::Parse(e)
    }
}

impl From<KernelError> for InterfaceError {
    fn from(e: KernelError) -> Self {
        InterfaceError::Kernel(e)
    }
}