lolli_core/
sequent.rs

1//! Sequent representation for linear logic.
2//!
3//! This module provides sequent data structures for both one-sided and two-sided sequents.
4
5use crate::Formula;
6
7/// A one-sided sequent ⊢ Γ.
8///
9/// We use a zone-based representation for focused proof search:
10/// - Linear zone: formulas that must be used exactly once
11/// - Unrestricted zone: formulas under ? that can be reused
12#[derive(Clone, Debug, PartialEq, Eq, Hash)]
13pub struct Sequent {
14    /// Linear hypotheses (multiset, represented as Vec)
15    pub linear: Vec<Formula>,
16
17    /// Unrestricted hypotheses (under ?)
18    pub unrestricted: Vec<Formula>,
19
20    /// Currently focused formula (if any)
21    pub focus: Option<Formula>,
22}
23
24impl Sequent {
25    /// Create a new sequent from a list of formulas.
26    pub fn new(formulas: Vec<Formula>) -> Self {
27        Sequent {
28            linear: formulas,
29            unrestricted: vec![],
30            focus: None,
31        }
32    }
33
34    /// Check if sequent is empty (proven).
35    pub fn is_empty(&self) -> bool {
36        self.linear.is_empty() && self.focus.is_none()
37    }
38
39    /// Focus on a formula at the given index.
40    pub fn focus_on(&self, idx: usize) -> Option<Sequent> {
41        if idx >= self.linear.len() {
42            return None;
43        }
44
45        let mut new_linear = self.linear.clone();
46        let focused = new_linear.remove(idx);
47
48        Some(Sequent {
49            linear: new_linear,
50            unrestricted: self.unrestricted.clone(),
51            focus: Some(focused),
52        })
53    }
54
55    /// Unfocus, returning formula to linear zone.
56    pub fn unfocus(&self) -> Sequent {
57        let mut new_linear = self.linear.clone();
58        if let Some(f) = &self.focus {
59            new_linear.push(f.clone());
60        }
61
62        Sequent {
63            linear: new_linear,
64            unrestricted: self.unrestricted.clone(),
65            focus: None,
66        }
67    }
68
69    /// Pretty print the sequent.
70    pub fn pretty(&self) -> String {
71        let formulas: Vec<String> = self.linear.iter().map(|f| f.pretty()).collect();
72        format!("⊢ {}", formulas.join(", "))
73    }
74}
75
76/// A two-sided sequent Γ ⊢ Δ (for user-facing API).
77#[derive(Clone, Debug, PartialEq, Eq)]
78pub struct TwoSidedSequent {
79    /// Left side of the turnstile (antecedent)
80    pub antecedent: Vec<Formula>,
81    /// Right side of the turnstile (succedent)
82    pub succedent: Vec<Formula>,
83}
84
85impl TwoSidedSequent {
86    /// Create a new two-sided sequent.
87    pub fn new(antecedent: Vec<Formula>, succedent: Vec<Formula>) -> Self {
88        TwoSidedSequent {
89            antecedent,
90            succedent,
91        }
92    }
93
94    /// Convert to one-sided: Γ ⊢ Δ becomes ⊢ Γ⊥, Δ
95    pub fn to_one_sided(&self) -> Sequent {
96        let mut formulas: Vec<Formula> = self.antecedent.iter().map(|f| f.negate()).collect();
97        formulas.extend(self.succedent.clone());
98
99        Sequent::new(formulas)
100    }
101
102    /// Pretty print the sequent.
103    pub fn pretty(&self) -> String {
104        let left: Vec<String> = self.antecedent.iter().map(|f| f.pretty()).collect();
105        let right: Vec<String> = self.succedent.iter().map(|f| f.pretty()).collect();
106        format!("{} ⊢ {}", left.join(", "), right.join(", "))
107    }
108}
109
110#[cfg(test)]
111mod tests {
112    use super::*;
113
114    #[test]
115    fn test_two_sided_to_one_sided() {
116        let seq = TwoSidedSequent::new(
117            vec![Formula::Atom("A".to_string())],
118            vec![Formula::Atom("B".to_string())],
119        );
120
121        let one_sided = seq.to_one_sided();
122        assert_eq!(one_sided.linear.len(), 2);
123        assert_eq!(one_sided.linear[0], Formula::NegAtom("A".to_string()));
124        assert_eq!(one_sided.linear[1], Formula::Atom("B".to_string()));
125    }
126
127    #[test]
128    fn test_focus_unfocus() {
129        let seq = Sequent::new(vec![
130            Formula::Atom("A".to_string()),
131            Formula::Atom("B".to_string()),
132        ]);
133
134        let focused = seq.focus_on(0).unwrap();
135        assert_eq!(focused.focus, Some(Formula::Atom("A".to_string())));
136        assert_eq!(focused.linear.len(), 1);
137
138        let unfocused = focused.unfocus();
139        assert_eq!(unfocused.linear.len(), 2);
140        assert!(unfocused.focus.is_none());
141    }
142}
lolli_core/sequent.rs

lolli_core/
sequent.rs
