Add unified type-system decoration framework and Sigma types

Author: hyperpolymath

src/rust/agent/explanations.rs

@@ -301,6 +301,18 @@ impl ExplanationGenerator {
                     self.format_term(body)
                 )
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                format!(
+                    "∃{}:{}. {}",
+                    param,
+                    self.format_term(param_type),
+                    self.format_term(body)
+                )
+            },
             Term::App { func, args } => {
                 let args_str: Vec<_> = args.iter().map(|a| self.format_term(a)).collect();
                 format!("({} {})", self.format_term(func), args_str.join(" "))

src/rust/aspect.rs

@@ -417,6 +417,9 @@ pub struct TheoremFeatures {
     /// Pi type (dependent function) count
     pub pi_count: usize,
 
+    /// Sigma type (dependent pair) count
+    pub sigma_count: usize,
+
     /// Universe levels used
     pub universe_levels: HashSet<usize>,
 
@@ -650,6 +653,9 @@ impl RuleBasedTagger {
             },
             Term::Pi {
                 param_type, body, ..
+            }
+            | Term::Sigma {
+                param_type, body, ..
             } => {
                 self.extract_symbols_recursive(param_type, symbols);
                 self.extract_symbols_recursive(body, symbols);
@@ -746,6 +752,11 @@ impl AspectTagger for RuleBasedTagger {
             total_matches += features.pi_count;
         }
 
+        if features.sigma_count > 0 {
+            *aspect_counts.entry(Aspect::DependentTypes).or_insert(0) += features.sigma_count;
+            total_matches += features.sigma_count;
+        }
+
         if !features.universe_levels.is_empty() {
             *aspect_counts.entry(Aspect::Universes).or_insert(0) += 1;
             total_matches += 1;
@@ -807,6 +818,13 @@ impl RuleBasedTagger {
                 self.analyze_term(param_type, features, depth + 1);
                 self.analyze_term(body, features, depth + 1);
             },
+            Term::Sigma {
+                param_type, body, ..
+            } => {
+                features.sigma_count += 1;
+                self.analyze_term(param_type, features, depth + 1);
+                self.analyze_term(body, features, depth + 1);
+            },
             Term::Universe(level) | Term::Type(level) | Term::Sort(level) => {
                 features.universe_levels.insert(*level);
             },

src/rust/core.rs

@@ -3,6 +3,7 @@
 
 //! Core types and abstractions for ECHIDNA theorem proving
 
+use crate::types::TypeInfo;
 use serde::{Deserialize, Serialize};
 use std::collections::HashMap;
 use std::fmt;
@@ -33,6 +34,17 @@ pub enum Term {
         body: Box<Term>,
     },
 
+    /// Dependent pair / sum (Sigma type) Σ(x: A). B
+    ///
+    /// Represents dependent pairs where the type of the second component may
+    /// depend on the value of the first. Non-dependent pairs are expressible
+    /// as `Sigma { body }` where `body` does not mention `param`.
+    Sigma {
+        param: String,
+        param_type: Box<Term>,
+        body: Box<Term>,
+    },
+
     /// Type universe at level
     Type(usize),
 
@@ -121,6 +133,13 @@ impl fmt::Display for Term {
             } => {
                 write!(f, "(Π {}: {}. {})", param, param_type, body)
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                write!(f, "(Σ {}: {}. {})", param, param_type, body)
+            },
             Term::Type(level) => write!(f, "Type{}", level),
             Term::Sort(level) => write!(f, "Sort{}", level),
             Term::Universe(level) => write!(f, "Type{}", level),
@@ -190,6 +209,26 @@ pub struct Hypothesis {
 
     /// Optional body (for definitions)
     pub body: Option<Term>,
+
+    /// Optional native type-system decoration (multiplicity, effects, modality,
+    /// refinement, semiring, …). `None` is semantically equivalent to a plain
+    /// unannotated hypothesis — backends that don't understand the decoration
+    /// safely ignore it.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub type_info: Option<TypeInfo>,
+}
+
+impl Hypothesis {
+    /// Construct a plain hypothesis with no type decoration.
+    pub fn new(name: impl Into<String>, ty: Term) -> Self {
+        Self { name: name.into(), ty, body: None, type_info: None }
+    }
+
+    /// Attach a [`TypeInfo`] decoration.
+    pub fn with_type_info(mut self, info: TypeInfo) -> Self {
+        self.type_info = Some(info);
+        self
+    }
 }
 
 /// Proof context with available premises
@@ -223,13 +262,47 @@ pub struct Definition {
     pub name: String,
     pub ty: Term,
     pub body: Term,
+
+    /// Optional native type-system decoration (see [`TypeInfo`]).
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub type_info: Option<TypeInfo>,
+}
+
+impl Definition {
+    /// Construct a plain definition with no type decoration.
+    pub fn new(name: impl Into<String>, ty: Term, body: Term) -> Self {
+        Self { name: name.into(), ty, body, type_info: None }
+    }
+
+    /// Attach a [`TypeInfo`] decoration.
+    pub fn with_type_info(mut self, info: TypeInfo) -> Self {
+        self.type_info = Some(info);
+        self
+    }
 }
 
 /// A variable declaration
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct Variable {
     pub name: String,
     pub ty: Term,
+
+    /// Optional native type-system decoration (see [`TypeInfo`]).
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub type_info: Option<TypeInfo>,
+}
+
+impl Variable {
+    /// Construct a plain variable with no type decoration.
+    pub fn new(name: impl Into<String>, ty: Term) -> Self {
+        Self { name: name.into(), ty, type_info: None }
+    }
+
+    /// Attach a [`TypeInfo`] decoration.
+    pub fn with_type_info(mut self, info: TypeInfo) -> Self {
+        self.type_info = Some(info);
+        self
+    }
 }
 
 /// A proof tactic/command

src/rust/gnn/embeddings.rs

@@ -350,6 +350,7 @@ fn term_kind_index(term: &Term) -> usize {
         Term::Hole(_) => 10,
         Term::Meta(_) => 11,
         Term::ProverSpecific { .. } => 12,
+        Term::Sigma { .. } => 13,
     }
 }
 
@@ -367,7 +368,8 @@ fn term_depth(term: &Term) -> usize {
             let pt = param_type.as_ref().map(|t| term_depth(t)).unwrap_or(0);
             1 + pt.max(term_depth(body))
         }
-        Term::Pi { param_type, body, .. } => {
+        Term::Pi { param_type, body, .. }
+        | Term::Sigma { param_type, body, .. } => {
             1 + term_depth(param_type).max(term_depth(body))
         }
         Term::Let { ty, value, body, .. } => {
@@ -394,7 +396,7 @@ fn term_arity(term: &Term) -> usize {
         | Term::Universe(_) | Term::Hole(_) | Term::Meta(_) | Term::ProverSpecific { .. } => 0,
         Term::App { args, .. } => 1 + args.len(), // func + args
         Term::Lambda { param_type, .. } => if param_type.is_some() { 2 } else { 1 },
-        Term::Pi { .. } => 2, // param_type + body
+        Term::Pi { .. } | Term::Sigma { .. } => 2, // param_type + body
         Term::Let { ty, .. } => if ty.is_some() { 3 } else { 2 },
         Term::Match { branches, .. } => 1 + branches.len(),
         Term::Fix { ty, .. } => if ty.is_some() { 2 } else { 1 },

src/rust/gnn/graph.rs

@@ -372,6 +372,23 @@ impl ProofGraphBuilder {
                 }
                 Some(nid)
             }
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                let label = format!("sigma_{}", param);
+                let nid = self.add_node(NodeKind::Binder, &label, depth);
+                self.add_edge(parent_id, nid, EdgeKind::Contains, 1.0);
+
+                if let Some(tid) = self.expand_term(param_type, nid, depth + 1) {
+                    self.add_edge(nid, tid, EdgeKind::HasType, 1.0);
+                }
+                if let Some(bid) = self.expand_term(body, nid, depth + 1) {
+                    self.add_edge(nid, bid, EdgeKind::BindsOver, 1.0);
+                }
+                Some(nid)
+            }
             Term::Type(level) | Term::Sort(level) | Term::Universe(level) => {
                 let label = format!("Type{}", level);
                 let nid = self.add_or_get_node(NodeKind::TypeExpr, &label, depth);
@@ -642,6 +659,7 @@ mod tests {
             name: "h_nat".to_string(),
             ty: Term::Const("Nat".to_string()),
             body: None,
+            type_info: None,
         };
 
         let theorem = Theorem {
@@ -687,6 +705,7 @@ mod tests {
                 variables: vec![Variable {
                     name: "n".to_string(),
                     ty: Term::Const("Nat".to_string()),
+                    type_info: None,
                 }],
             },
             proof_script: Vec::new(),

src/rust/gnn/guided_search.rs

@@ -381,6 +381,7 @@ mod tests {
                     name: "h".to_string(),
                     ty: Term::Const("Nat".to_string()),
                     body: None,
+                    type_info: None,
                 }],
             }],
             context: Context {
@@ -390,6 +391,7 @@ mod tests {
                 variables: vec![Variable {
                     name: "n".to_string(),
                     ty: Term::Const("Nat".to_string()),
+                    type_info: None,
                 }],
             },
             proof_script: Vec::new(),

src/rust/lib.rs

@@ -26,6 +26,7 @@ pub mod parsers;
 pub mod proof_encoding; // CBOR encoding + proof identity hashing
 pub mod proof_search; // Chapel parallel proof search (optional feature)
 pub mod provers;
+pub mod types; // Native type-system decorations (multiplicity, effects, modality, temporal, semiring, …)
 pub mod verification;
 #[cfg(feature = "verisim")]
 pub mod verisim_bridge; // VeriSimDB 8-modality octad integration

src/rust/provers/abc.rs

@@ -269,6 +269,7 @@ impl AbcBackend {
                         name: input_name.to_string(),
                         ty: Term::Const("BLIF_INPUT".to_string()),
                         body: Term::Const(input_name.to_string()),
+                        type_info: None,
                     });
                 }
             }

src/rust/provers/acl2.rs

@@ -980,6 +980,18 @@ impl ACL2Backend {
                     ])
                 }
             },
+            Term::Sigma {
+                param: _,
+                param_type,
+                body,
+            } => {
+                // ACL2 has no dependent pairs; approximate with (and A B).
+                SExp::List(vec![
+                    SExp::Atom("and".to_string()),
+                    self.term_to_sexp(param_type),
+                    self.term_to_sexp(body),
+                ])
+            },
             Term::Let {
                 name, value, body, ..
             } => SExp::List(vec![
@@ -1250,6 +1262,7 @@ impl ProverBackend for ACL2Backend {
                         name,
                         ty: Term::Universe(0), // ACL2 doesn't have explicit types
                         body: body_term,
+                        type_info: None,
                     });
                 },
                 ACL2Event::Defthm {
@@ -1291,6 +1304,7 @@ impl ProverBackend for ACL2Backend {
                         name,
                         ty: Term::Universe(0),
                         body: value_term,
+                        type_info: None,
                     });
                 },
                 _ => {},

src/rust/provers/agda.rs

@@ -134,6 +134,16 @@ impl AgdaBackend {
                 let body_str = self.term_to_agda(body);
                 format!("({} : {}) → {}", param, param_ty_str, body_str)
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                // Agda: Σ A λ x → B  (standard-library)
+                let param_ty_str = self.term_to_agda(param_type);
+                let body_str = self.term_to_agda(body);
+                format!("Σ {} λ {} → {}", param_ty_str, param, body_str)
+            },
             Term::Universe(level) | Term::Type(level) => {
                 if *level == 0 {
                     "Set".to_string()
@@ -263,6 +273,7 @@ impl ProverBackend for AgdaBackend {
                         name: name.clone(),
                         ty: type_term.clone(),
                         body: type_term,
+                        type_info: None,
                     });
                 },
                 AgdaDecl::TypeSig { name, ty } => {
@@ -318,6 +329,7 @@ impl ProverBackend for AgdaBackend {
                         name: param_name,
                         ty: Term::Universe(0),
                         body: None,
+                        type_info: None,
                     });
                 }
                 Ok(TacticResult::Success(new_state))