diff --git a/src/rust/agent/explanations.rs b/src/rust/agent/explanations.rs index c5181c7..e3f17a8 100644 --- a/src/rust/agent/explanations.rs +++ b/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(" ")) diff --git a/src/rust/aspect.rs b/src/rust/aspect.rs index 67d6ab7..20175f1 100644 --- a/src/rust/aspect.rs +++ b/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, @@ -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); }, diff --git a/src/rust/core.rs b/src/rust/core.rs index c12103a..78a40c9 100644 --- a/src/rust/core.rs +++ b/src/rust/core.rs @@ -33,6 +33,13 @@ pub enum Term { body: Box, }, + /// Dependent pair / sum (Sigma type) Σ(x: A). B + Sigma { + param: String, + param_type: Box, + body: Box, + }, + /// Type universe at level Type(usize), @@ -121,6 +128,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), @@ -189,6 +203,10 @@ pub struct Hypothesis { /// Optional body (for definitions) pub body: Option, + + /// Optional native type-system decoration. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub type_info: Option, } /// Proof context with available premises @@ -222,6 +240,8 @@ pub struct Definition { pub name: String, pub ty: Term, pub body: Term, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub type_info: Option, } /// A variable declaration @@ -229,6 +249,8 @@ pub struct Definition { pub struct Variable { pub name: String, pub ty: Term, + #[serde(default, skip_serializing_if = "Option::is_none")] + pub type_info: Option, } /// A proof tactic/command diff --git a/src/rust/exchange/dedukti.rs b/src/rust/exchange/dedukti.rs index 3849875..04bf345 100644 --- a/src/rust/exchange/dedukti.rs +++ b/src/rust/exchange/dedukti.rs @@ -211,6 +211,18 @@ impl DeduktiExporter { Self::term_to_dedukti(body) ) }, + Term::Sigma { + param, + param_type, + body, + } => { + format!( + "(dk_sigma {} ({} => {}))", + Self::term_to_dedukti(param_type), + param, + Self::term_to_dedukti(body) + ) + }, Term::Type(level) => format!("Type {}", level), Term::Sort(level) => format!("Sort {}", level), Term::Universe(level) => format!("Type {}", level), @@ -224,6 +236,32 @@ impl DeduktiExporter { if trimmed.starts_with('(') && trimmed.ends_with(')') { // Unwrap parentheses and recurse Self::dedukti_to_term(&trimmed[1..trimmed.len() - 1]) + } else if trimmed.starts_with("dk_sigma ") { + // Sigma type: dk_sigma A (x => B) + let rest = trimmed.trim_start_matches("dk_sigma ").trim(); + // Split into the type part and the binder part (x => B) + if let Some(paren_start) = rest.find('(') { + let type_part = rest[..paren_start].trim(); + let binder_part = rest[paren_start..].trim(); + let inner = if binder_part.starts_with('(') && binder_part.ends_with(')') { + &binder_part[1..binder_part.len() - 1] + } else { + binder_part + }; + if let Some(arrow_pos) = inner.find("=>") { + let param = inner[..arrow_pos].trim().to_string(); + let body_str = inner[arrow_pos + 2..].trim(); + Term::Sigma { + param, + param_type: Box::new(Self::dedukti_to_term(type_part)), + body: Box::new(Self::dedukti_to_term(body_str)), + } + } else { + Term::Const(trimmed.to_string()) + } + } else { + Term::Const(trimmed.to_string()) + } } else if trimmed.contains("->") { // Pi type: A -> B let parts: Vec<&str> = trimmed.splitn(2, "->").collect(); @@ -416,6 +454,28 @@ mod tests { assert_eq!(dk, "x"); } + #[test] + fn test_term_to_dedukti_sigma() { + let term = Term::Sigma { + param: "x".to_string(), + param_type: Box::new(Term::Const("Nat".to_string())), + body: Box::new(Term::Const("Prop".to_string())), + }; + let dk = DeduktiExporter::term_to_dedukti(&term); + assert!(dk.contains("dk_sigma"), "Sigma should render as dk_sigma, got: {}", dk); + assert!(dk.contains("Nat"), "Sigma param type should appear, got: {}", dk); + } + + #[test] + fn test_dedukti_to_term_sigma() { + let dk = "dk_sigma Nat (x => Prop)"; + let term = DeduktiExporter::dedukti_to_term(dk); + match term { + Term::Sigma { ref param, .. } => assert_eq!(param, "x"), + _ => panic!("Expected Sigma term, got: {:?}", term), + } + } + #[test] fn test_import_with_definition() { let module = DeduktiModule { diff --git a/src/rust/gnn/embeddings.rs b/src/rust/gnn/embeddings.rs index 84aca22..df82d41 100644 --- a/src/rust/gnn/embeddings.rs +++ b/src/rust/gnn/embeddings.rs @@ -184,9 +184,11 @@ impl TermFeatureExtractor { // Feature [29]: Contains quantifier (forall, exists, pi) if offset < FEATURE_DIM { features[offset] = if node.label.contains("pi_") + || node.label.contains("sigma_") || node.label.contains("forall") || node.label.contains("exists") || node.label.contains("Pi") + || node.label.contains("Sigma") { 1.0 } else { @@ -304,6 +306,8 @@ fn infer_term_kind_from_label(label: &str) -> usize { 3 // Lambda } else if label.starts_with("pi_") { 4 // Pi + } else if label.starts_with("sigma_") { + 13 // Sigma } else if label.starts_with("let_") { 7 // Let } else if label.starts_with("fix_") { @@ -344,6 +348,7 @@ fn term_kind_index(term: &Term) -> usize { Term::Hole(_) => 10, Term::Meta(_) => 11, Term::ProverSpecific { .. } => 12, + Term::Sigma { .. } => 13, } } @@ -370,6 +375,9 @@ fn term_depth(term: &Term) -> usize { }, Term::Pi { param_type, body, .. + } + | Term::Sigma { + param_type, body, .. } => 1 + term_depth(param_type).max(term_depth(body)), Term::Let { ty, value, body, .. @@ -417,7 +425,7 @@ fn term_arity(term: &Term) -> usize { 1 } }, - Term::Pi { .. } => 2, // param_type + body + Term::Pi { .. } | Term::Sigma { .. } => 2, // param_type + body Term::Let { ty, .. } => { if ty.is_some() { 3 diff --git a/src/rust/gnn/graph.rs b/src/rust/gnn/graph.rs index 3a0ad66..ea4f39e 100644 --- a/src/rust/gnn/graph.rs +++ b/src/rust/gnn/graph.rs @@ -17,7 +17,7 @@ use serde::{Deserialize, Serialize}; use std::collections::HashMap; -use crate::core::{Context, Goal, Hypothesis, ProofState, Term, Theorem}; +use crate::core::{Context, Definition, Goal, Hypothesis, ProofState, Term, Theorem}; /// Kind of node in the proof graph. /// @@ -63,6 +63,12 @@ pub enum EdgeKind { DependsOn, /// Reverse of DependsOn (premise is useful for goal) UsefulFor, + /// Source has the target as its QTT multiplicity annotation + HasMultiplicity, + /// Source has the target as its algebraic effect annotation + HasEffect, + /// Source has the target as its modal decoration + HasModality, } /// A single node in the proof graph. @@ -185,18 +191,25 @@ impl ProofGraphBuilder { // Phase 2: Add hypothesis nodes from context let hyp_ids = self.add_hypotheses_from_context(&state.context); + // Phase 2b: Add definition nodes from context + let def_ids = self.add_definitions_from_context(&state.context); + // Phase 3: Add premise/theorem nodes from context for theorem in &state.context.theorems { let pid = self.add_premise(theorem); premise_node_ids.push(pid); } - // Phase 4: Add dependency edges from goals to hypotheses/premises + // Phase 4: Add dependency edges from goals to hypotheses/definitions/premises if let Some(gid) = goal_node_id { for &hid in &hyp_ids { self.add_edge(gid, hid, EdgeKind::DependsOn, 1.0); self.add_edge(hid, gid, EdgeKind::UsefulFor, 1.0); } + for &did in &def_ids { + self.add_edge(gid, did, EdgeKind::DependsOn, 0.9); + self.add_edge(did, gid, EdgeKind::UsefulFor, 0.9); + } for &pid in &premise_node_ids { self.add_edge(gid, pid, EdgeKind::DependsOn, 0.8); self.add_edge(pid, gid, EdgeKind::UsefulFor, 0.8); @@ -278,6 +291,11 @@ impl ProofGraphBuilder { self.expand_term(body, hid, 1); } + // Wire type_info annotations as edges + if let Some(ref info) = hyp.type_info { + self.add_type_info_edges(hid, info); + } + hid } @@ -288,11 +306,49 @@ impl ProofGraphBuilder { let label = format!("{}: {}", var.name, var.ty); let vid = self.add_node(NodeKind::Hypothesis, &label, 0); self.expand_term(&var.ty, vid, 1); + + // Wire type_info annotations as edges + if let Some(ref info) = var.type_info { + self.add_type_info_edges(vid, info); + } + ids.push(vid); } ids } + /// Add definition nodes from the global context. + fn add_definitions_from_context(&mut self, ctx: &Context) -> Vec { + let mut ids = Vec::new(); + for def in &ctx.definitions { + let did = self.add_definition(def); + ids.push(did); + } + ids + } + + /// Add a definition node. + fn add_definition(&mut self, def: &Definition) -> usize { + let label = format!("{}: {}", def.name, def.ty); + let did = self.add_node(NodeKind::Hypothesis, &label, 0); + + // Expand the definition type + let type_id = self.expand_term(&def.ty, did, 1); + if let Some(tid) = type_id { + self.add_edge(did, tid, EdgeKind::HasType, 1.0); + } + + // Expand the definition body + self.expand_term(&def.body, did, 1); + + // Wire type_info annotations as edges + if let Some(ref info) = def.type_info { + self.add_type_info_edges(did, info); + } + + did + } + /// Add a premise (theorem/lemma) node. fn add_premise(&mut self, theorem: &Theorem) -> usize { let label = format!("{}: {}", theorem.name, theorem.statement); @@ -372,6 +428,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); @@ -442,6 +515,32 @@ impl ProofGraphBuilder { } } + /// Add edges from a node to represent its [`TypeInfo`] annotations. + /// + /// Creates labelled subterm nodes for multiplicity, effect, and modality + /// decorations and connects them with the appropriate edge kind. + fn add_type_info_edges(&mut self, node_id: usize, info: &crate::types::TypeInfo) { + if let Some(ref mult) = info.multiplicity { + let label = format!("mult:{:?}", mult); + let mid = self.add_node(NodeKind::Subterm, &label, 1); + self.add_edge(node_id, mid, EdgeKind::HasMultiplicity, 1.0); + } + + if !info.effects.is_empty() { + for eff in &info.effects.effects { + let label = format!("effect:{:?}", eff); + let eid = self.add_node(NodeKind::Subterm, &label, 1); + self.add_edge(node_id, eid, EdgeKind::HasEffect, 1.0); + } + } + + if let Some(ref modality) = info.modality { + let label = format!("modality:{:?}", modality); + let mid = self.add_node(NodeKind::Subterm, &label, 1); + self.add_edge(node_id, mid, EdgeKind::HasModality, 1.0); + } + } + /// Add shared-structure edges between premise nodes that share constants. /// /// Two premises sharing named constants likely have semantic overlap, diff --git a/src/rust/lib.rs b/src/rust/lib.rs index dce0444..3e14daa 100644 --- a/src/rust/lib.rs +++ b/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; pub mod vcl_ut; pub mod verification; #[cfg(feature = "verisim")] diff --git a/src/rust/provers/abc.rs b/src/rust/provers/abc.rs index 83a7960..da267f9 100644 --- a/src/rust/provers/abc.rs +++ b/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, }); } } diff --git a/src/rust/provers/acl2.rs b/src/rust/provers/acl2.rs index 70c28fc..d68fa90 100644 --- a/src/rust/provers/acl2.rs +++ b/src/rust/provers/acl2.rs @@ -981,6 +981,16 @@ impl ACL2Backend { ]) } }, + Term::Sigma { + param_type, body, .. + } => { + // Sigma types approximated as conjunction (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![ @@ -1251,6 +1261,7 @@ impl ProverBackend for ACL2Backend { name, ty: Term::Universe(0), // ACL2 doesn't have explicit types body: body_term, + type_info: None, }); }, ACL2Event::Defthm { @@ -1292,6 +1303,7 @@ impl ProverBackend for ACL2Backend { name, ty: Term::Universe(0), body: value_term, + type_info: None, }); }, _ => {}, diff --git a/src/rust/provers/agda.rs b/src/rust/provers/agda.rs index 27907cf..2346ccf 100644 --- a/src/rust/provers/agda.rs +++ b/src/rust/provers/agda.rs @@ -134,6 +134,15 @@ impl AgdaBackend { let body_str = self.term_to_agda(body); format!("({} : {}) → {}", param, param_ty_str, body_str) }, + Term::Sigma { + param, + param_type, + body, + } => { + 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 +272,7 @@ impl ProverBackend for AgdaBackend { name: name.clone(), ty: type_term.clone(), body: type_term, + type_info: None, }); }, AgdaDecl::TypeSig { name, ty } => { @@ -318,6 +328,7 @@ impl ProverBackend for AgdaBackend { name: param_name, ty: Term::Universe(0), body: None, + type_info: None, }); } Ok(TacticResult::Success(new_state)) diff --git a/src/rust/provers/alloy.rs b/src/rust/provers/alloy.rs index e87a734..a0a76ec 100644 --- a/src/rust/provers/alloy.rs +++ b/src/rust/provers/alloy.rs @@ -161,6 +161,7 @@ impl AlloyBackend { name: trimmed.to_string(), ty: Term::Const("ALLOY_DEF".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } @@ -170,6 +171,7 @@ impl AlloyBackend { name: trimmed.to_string(), ty: Term::Const("ALLOY_DEF".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } diff --git a/src/rust/provers/coq.rs b/src/rust/provers/coq.rs index 80f256b..e36c81d 100644 --- a/src/rust/provers/coq.rs +++ b/src/rust/provers/coq.rs @@ -866,6 +866,7 @@ impl ProverBackend for CoqBackend { name, ty: def_type, body, + type_info: None, }); }, CoqStatement::Tactic(tactic_str) => { diff --git a/src/rust/provers/cvc5.rs b/src/rust/provers/cvc5.rs index 127a608..31aa957 100644 --- a/src/rust/provers/cvc5.rs +++ b/src/rust/provers/cvc5.rs @@ -427,6 +427,7 @@ impl CVC5Backend { state.context.variables.push(crate::core::Variable { name: name.to_string(), ty: Term::Const(ty.trim().to_string()), + type_info: None, }); } continue; @@ -454,6 +455,7 @@ impl CVC5Backend { state.context.variables.push(crate::core::Variable { name: name.to_string(), ty: Term::Const(return_ty.to_string()), + type_info: None, }); } } diff --git a/src/rust/provers/fstar.rs b/src/rust/provers/fstar.rs index fd2cbc3..1a26c42 100644 --- a/src/rust/provers/fstar.rs +++ b/src/rust/provers/fstar.rs @@ -17,6 +17,7 @@ use tokio::process::Command; use super::{ProverBackend, ProverConfig, ProverKind}; use crate::core::{Goal, ProofState, Tactic, TacticResult, Term}; +use crate::types::{Effect, TypeInfo}; /// F* backend pub struct FStarBackend { @@ -33,12 +34,51 @@ impl FStarBackend { for (i, axiom) in state.context.axioms.iter().enumerate() { input.push_str(&format!("assume val axiom_{} : {}\n", i, axiom)); } + // Emit definitions with effect and refinement annotations from TypeInfo + for def in &state.context.definitions { + let effect_str = def + .type_info + .as_ref() + .map(Self::effect_to_fstar) + .unwrap_or_default(); + let refinement_str = def + .type_info + .as_ref() + .and_then(|ti| ti.refinement.as_ref()) + .map(|pred| format!("{{v:{} | {}}}", def.ty, pred)) + .unwrap_or_else(|| format!("{}", def.ty)); + input.push_str(&format!("val {} : {}{}\n", def.name, effect_str, refinement_str)); + } if let Some(goal) = state.goals.first() { input.push_str(&format!("\nval goal : {}\n", goal.target)); } Ok(input) } + /// Convert effect row from [`TypeInfo`] to an F* effect annotation prefix. + fn effect_to_fstar(ti: &TypeInfo) -> String { + if ti.effects.is_empty() { + return String::new(); + } + let effect_name = ti + .effects + .effects + .first() + .map(|e| match e { + Effect::Pure | Effect::Tot => "Tot", + Effect::IO => "IO", + Effect::State => "ST", + Effect::Exception => "Exn", + Effect::Div => "Div", + Effect::Ghost => "GTot", + Effect::NonDet => "ALL", + Effect::Async => "ALL", + Effect::Custom(s) => s.as_str(), + }) + .unwrap_or("Tot"); + format!("{} ", effect_name) + } + fn parse_result(&self, output: &str) -> Result { let lower = output.to_lowercase(); if lower.contains("verified") || lower.contains("all verification conditions discharged") { diff --git a/src/rust/provers/hol4.rs b/src/rust/provers/hol4.rs index 6744ed5..fb5c236 100644 --- a/src/rust/provers/hol4.rs +++ b/src/rust/provers/hol4.rs @@ -1502,6 +1502,16 @@ impl Hol4Backend { var_type: Some(Self::term_to_type(param_type)), body: Box::new(Self::term_to_hol4(body)), }, + Term::Sigma { + param, + param_type, + body, + } => HOL4Term::Quant { + quantifier: HOL4Quantifier::Exists, + var: param.clone(), + var_type: Some(Self::term_to_type(param_type)), + body: Box::new(Self::term_to_hol4(body)), + }, Term::Let { name, value, body, .. } => HOL4Term::Let { @@ -2166,6 +2176,7 @@ impl ProverBackend for Hol4Backend { name: name.clone(), ty: Self::hol4_to_term(body), body: None, + type_info: None, }); }, _ => {}, diff --git a/src/rust/provers/hol_light.rs b/src/rust/provers/hol_light.rs index 97fc369..17bb3a8 100644 --- a/src/rust/provers/hol_light.rs +++ b/src/rust/provers/hol_light.rs @@ -262,6 +262,18 @@ impl HolLightBackend { self.term_to_hol(body) ) }, + Term::Sigma { + param, + param_type, + body, + } => { + format!( + "(?{} : {}. {})", + param, + self.term_to_hol(param_type), + self.term_to_hol(body) + ) + }, Term::Universe(level) | Term::Type(level) => format!("Type{}", level), Term::Sort(level) => format!("Sort{}", level), Term::Let { @@ -452,6 +464,7 @@ impl ProverBackend for HolLightBackend { data: serde_json::json!(def.def_type.clone()), }, body: def_term, + type_info: None, }); } diff --git a/src/rust/provers/idris2.rs b/src/rust/provers/idris2.rs index 441a99d..f45d4f5 100644 --- a/src/rust/provers/idris2.rs +++ b/src/rust/provers/idris2.rs @@ -30,6 +30,7 @@ use crate::core::{ Theorem, }; use crate::provers::{ProverBackend, ProverConfig, ProverKind}; +use crate::types::Multiplicity; /// Idris 2 backend implementation pub struct Idris2Backend { @@ -105,17 +106,6 @@ enum Idris2Term { AutoImplicit(String, Box), } -/// Quantitative type theory multiplicities -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -enum Multiplicity { - /// Unrestricted (0, 1, or many uses) - Unrestricted, - /// Linear (exactly 1 use) - Linear, - /// Erased (0 uses at runtime) - Erased, -} - impl Idris2Backend { pub fn new(config: ProverConfig) -> Self { Idris2Backend { @@ -178,6 +168,17 @@ impl Idris2Backend { } } + /// Convert a [`Multiplicity`] to the Idris 2 QTT annotation string. + fn multiplicity_to_idris2(m: &Multiplicity) -> &'static str { + match m { + Multiplicity::Zero => "0", + Multiplicity::One | Multiplicity::Linear => "1", + Multiplicity::Omega | Multiplicity::Shared => "", + Multiplicity::Affine => "1", // closest QTT approximation + Multiplicity::Graded(_) => "", + } + } + /// Convert universal Term to Idris 2 syntax fn term_to_idris2(&self, term: &Term) -> String { match term { @@ -232,6 +233,15 @@ impl Idris2Backend { format!("({} : {}) -> {}", param, param_ty_str, body_str) } }, + Term::Sigma { + param, + param_type, + body, + } => { + let param_ty_str = self.term_to_idris2(param_type); + let body_str = self.term_to_idris2(body); + format!("({} : {} ** {})", param, param_ty_str, body_str) + }, Term::Type(level) | Term::Universe(level) => { if *level == 0 { "Type".to_string() @@ -495,6 +505,7 @@ impl ProverBackend for Idris2Backend { name: name.clone(), ty: self.parse_type_expr(&ty_str), body: Term::Const(name.clone()), + type_info: None, }); // Add constructors as theorems @@ -522,6 +533,7 @@ impl ProverBackend for Idris2Backend { name: name.clone(), ty: self.parse_type_expr(&ty_str), body: Term::Const(name.clone()), + type_info: None, }); // Add field projections @@ -557,6 +569,7 @@ impl ProverBackend for Idris2Backend { body: Box::new(Term::Type(0)), }, body: Term::Const(name.clone()), + type_info: None, }); // Methods as theorems @@ -616,6 +629,7 @@ impl ProverBackend for Idris2Backend { name: param_name.clone(), ty: Term::Type(0), // Placeholder body: None, + type_info: None, }); // Update goal target if it's a Pi type @@ -801,11 +815,17 @@ impl ProverBackend for Idris2Backend { output.push_str("import Data.Vect\n"); output.push_str("import Data.Nat\n\n"); - // Definitions + // Definitions (emit QTT multiplicity annotations when present) for def in &state.context.definitions { let ty_str = self.term_to_idris2(&def.ty); let body_str = self.term_to_idris2(&def.body); - output.push_str(&format!("{} : {}\n", def.name, ty_str)); + let mult_prefix = def + .type_info + .as_ref() + .and_then(|ti| ti.multiplicity.as_ref()) + .map(|m| format!("{} ", Self::multiplicity_to_idris2(m))) + .unwrap_or_default(); + output.push_str(&format!("{}{} : {}\n", mult_prefix, def.name, ty_str)); output.push_str(&format!("{} = {}\n\n", def.name, body_str)); } @@ -1196,7 +1216,7 @@ mod tests { // Test Pi type let pi_term = Idris2Term::Pi( "a".to_string(), - Multiplicity::Unrestricted, + Multiplicity::Omega, Box::new(Idris2Term::Type), Box::new(Idris2Term::Var("a".to_string())), ); diff --git a/src/rust/provers/isabelle.rs b/src/rust/provers/isabelle.rs index 97145b0..3fab082 100644 --- a/src/rust/provers/isabelle.rs +++ b/src/rust/provers/isabelle.rs @@ -428,6 +428,7 @@ impl ProverBackend for IsabelleBackend { name: "IH".to_string(), ty: goal.target.clone(), body: None, + type_info: None, }); hyps }, diff --git a/src/rust/provers/lean.rs b/src/rust/provers/lean.rs index 8df178b..04bcbf1 100644 --- a/src/rust/provers/lean.rs +++ b/src/rust/provers/lean.rs @@ -369,6 +369,18 @@ impl LeanBackend { self.term_to_lean(body) ) }, + Term::Sigma { + param, + param_type, + body, + } => { + format!( + "(({} : {}) × {})", + param, + self.term_to_lean(param_type), + self.term_to_lean(body) + ) + }, Term::Let { name, ty, @@ -653,6 +665,7 @@ impl LeanBackend { name: name.clone(), ty: term_ty, body: term_val, + type_info: None, }); }, LeanDeclaration::Axiom { name, ty, .. } => { @@ -688,6 +701,7 @@ impl LeanBackend { name: h.name.clone(), ty: self.lean_expr_to_term(&h.ty), body: h.value.as_ref().map(|v| self.lean_expr_to_term(v)), + type_info: None, }) .collect(); @@ -1275,6 +1289,7 @@ impl ProverBackend for LeanBackend { name: h.name.clone(), ty: self.lean_expr_to_term(&h.ty), body: h.value.as_ref().map(|v| self.lean_expr_to_term(v)), + type_info: None, }) .collect(), }) diff --git a/src/rust/provers/metamath.rs b/src/rust/provers/metamath.rs index 60f3dae..4a9c3f2 100644 --- a/src/rust/provers/metamath.rs +++ b/src/rust/provers/metamath.rs @@ -327,6 +327,7 @@ impl ProverBackend for MetamathBackend { context.variables.push(Variable { name: var.clone(), ty: Term::Const(typecode.clone()), + type_info: None, }); }, _ => {}, diff --git a/src/rust/provers/mizar.rs b/src/rust/provers/mizar.rs index 19fdf51..eaaa140 100644 --- a/src/rust/provers/mizar.rs +++ b/src/rust/provers/mizar.rs @@ -284,6 +284,18 @@ impl MizarBackend { self.term_to_mizar(body) ) }, + Term::Sigma { + param, + param_type, + body, + } => { + format!( + "ex {} being {} st {}", + param, + self.term_to_mizar(param_type), + self.term_to_mizar(body) + ) + }, Term::Universe(level) | Term::Type(level) => format!("Type{}", level), Term::Sort(level) => format!("Sort{}", level), Term::Let { @@ -406,6 +418,7 @@ impl ProverBackend for MizarBackend { name: def.name.clone(), ty: def_type, body: def_body, + type_info: None, }); } @@ -448,6 +461,7 @@ impl ProverBackend for MizarBackend { name: hypothesis_name, ty: *param_type.clone(), body: None, + type_info: None, }); goal.target = *body.clone(); new_state.proof_script.push(tactic.clone()); diff --git a/src/rust/provers/nusmv.rs b/src/rust/provers/nusmv.rs index 06ba83e..c464b40 100644 --- a/src/rust/provers/nusmv.rs +++ b/src/rust/provers/nusmv.rs @@ -168,6 +168,7 @@ impl NuSMVBackend { name: trimmed.to_string(), ty: Term::Const("SMV_VAR".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } diff --git a/src/rust/provers/prism.rs b/src/rust/provers/prism.rs index b004c3d..41c34cf 100644 --- a/src/rust/provers/prism.rs +++ b/src/rust/provers/prism.rs @@ -185,6 +185,7 @@ impl PrismBackend { name: trimmed.to_string(), ty: Term::Const("PRISM_VAR".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } diff --git a/src/rust/provers/proverif.rs b/src/rust/provers/proverif.rs index 49d7292..ef82793 100644 --- a/src/rust/provers/proverif.rs +++ b/src/rust/provers/proverif.rs @@ -402,6 +402,7 @@ fn pv_definition(line: &str) -> Definition { name, ty: Term::Const("proverif_decl".to_string()), body: Term::Const(clean.to_string()), + type_info: None, } } diff --git a/src/rust/provers/pvs.rs b/src/rust/provers/pvs.rs index 4f1ae83..331bf92 100644 --- a/src/rust/provers/pvs.rs +++ b/src/rust/provers/pvs.rs @@ -2103,6 +2103,20 @@ impl PVSBackend { body: Box::new(Self::term_to_expr(body)), } }, + Term::Sigma { + param, + param_type, + body, + } => { + // Sigma types map to EXISTS in PVS + PVSExpr::Exists { + bindings: vec![PVSBinding { + name: param.clone(), + var_type: Box::new(Self::term_to_type(param_type)), + }], + body: Box::new(Self::term_to_expr(body)), + } + }, Term::Let { name, value, body, .. } => PVSExpr::Let { @@ -2702,6 +2716,7 @@ impl ProverBackend for PVSBackend { name: name.clone(), ty: Self::expr_to_term(formula), body: None, + type_info: None, }); }, PVSFormulaKind::Lemma @@ -2731,6 +2746,7 @@ impl ProverBackend for PVSBackend { name: format!("{}_def", name), ty: def_term, body: Some(Self::expr_to_term(def)), + type_info: None, }); }, PVSDeclaration::ConstDecl { diff --git a/src/rust/provers/tamarin.rs b/src/rust/provers/tamarin.rs index e568d54..c4a1dfb 100644 --- a/src/rust/provers/tamarin.rs +++ b/src/rust/provers/tamarin.rs @@ -203,6 +203,7 @@ impl TamarinBackend { name: "builtins".to_string(), ty: Term::Const("builtin-declaration".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } @@ -212,6 +213,7 @@ impl TamarinBackend { name: "functions".to_string(), ty: Term::Const("function-declaration".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } @@ -221,6 +223,7 @@ impl TamarinBackend { name: "equations".to_string(), ty: Term::Const("equation-declaration".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } @@ -353,6 +356,7 @@ impl ProverBackend for TamarinBackend { name: "builtins".to_string(), ty: Term::Const("builtin-declaration".to_string()), body: Term::Const(format!("builtins: {}", builtin_text)), + type_info: None, }); new_state.proof_script.push(tactic.clone()); Ok(TacticResult::Success(new_state)) diff --git a/src/rust/provers/tlc.rs b/src/rust/provers/tlc.rs index c20b5ee..580bdaa 100644 --- a/src/rust/provers/tlc.rs +++ b/src/rust/provers/tlc.rs @@ -171,6 +171,7 @@ impl TLCBackend { name: trimmed.to_string(), ty: Term::Const("TLA_OP".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } diff --git a/src/rust/provers/typed_wasm.rs b/src/rust/provers/typed_wasm.rs index 2496c80..ba2d3b4 100644 --- a/src/rust/provers/typed_wasm.rs +++ b/src/rust/provers/typed_wasm.rs @@ -941,6 +941,7 @@ impl TypedWasmBackend { name: format!("{}_witness", label), ty: Term::Const(format!("Witness({})", witness)), body: None, + type_info: None, }); } @@ -983,6 +984,7 @@ impl TypedWasmBackend { name: format!("region_{}", schema.name), ty: Term::Const("Schema".to_string()), body: fields_term, + type_info: None, }); } } diff --git a/src/rust/provers/uppaal.rs b/src/rust/provers/uppaal.rs index 77feced..0716b43 100644 --- a/src/rust/provers/uppaal.rs +++ b/src/rust/provers/uppaal.rs @@ -187,6 +187,7 @@ impl UppaalBackend { name: trimmed.to_string(), ty: Term::Const("UPPAAL_DECL".to_string()), body: Term::Const(trimmed.to_string()), + type_info: None, }); } @@ -289,6 +290,7 @@ impl ProverBackend for UppaalBackend { name: clock_name.clone(), ty: Term::Const("clock".to_string()), body: Term::Const(format!("clock {};", clock_name)), + type_info: None, }); new_state.proof_script.push(tactic.clone()); Ok(TacticResult::Success(new_state)) @@ -306,6 +308,7 @@ impl ProverBackend for UppaalBackend { name: chan_name.clone(), ty: Term::Const("chan".to_string()), body: Term::Const(format!("chan {};", chan_name)), + type_info: None, }); new_state.proof_script.push(tactic.clone()); Ok(TacticResult::Success(new_state)) diff --git a/src/rust/provers/z3.rs b/src/rust/provers/z3.rs index 2f3c988..6f01d69 100644 --- a/src/rust/provers/z3.rs +++ b/src/rust/provers/z3.rs @@ -702,6 +702,7 @@ impl SmtParser { state.context.variables.push(crate::core::Variable { name: name.clone(), ty: self.smt_to_term(&ty_term), + type_info: None, }); }, @@ -732,6 +733,7 @@ impl SmtParser { state.context.variables.push(crate::core::Variable { name: name.clone(), ty, + type_info: None, }); }, diff --git a/src/rust/vcl_ut.rs b/src/rust/vcl_ut.rs index 1689afa..26dc9e0 100644 --- a/src/rust/vcl_ut.rs +++ b/src/rust/vcl_ut.rs @@ -493,6 +493,7 @@ impl QueryExecutor { /// Find a specific proof by theorem name and optional prover. async fn execute_find_proof(&self, query: &ProofQuery) -> Result { + type_info: None, let theorem = query.theorem_name.as_deref().unwrap_or(""); #[cfg(feature = "verisim")]