#![cfg(feature = "repl")]
use super::counterexample::{Counterexample, CounterexampleGenerator};
use super::refinement::{RefinementChecker, RefinementType};
use super::smt::{SmtBackend, SmtQuery, SmtResult, SmtSolver};
use super::tactics::{Tactic, TacticLibrary, TacticSuggestion};
use anyhow::Result;
#[cfg(test)]
use proptest::prelude::*;
use rustyline::error::ReadlineError;
use rustyline::DefaultEditor;
use serde::{Deserialize, Serialize};
use std::collections::{HashMap, VecDeque};
use std::time::{Duration, Instant};
pub struct InteractiveProver {
session: ProverSession,
tactics: TacticLibrary,
smt: SmtSolver,
refinement_checker: RefinementChecker,
counterexample_gen: CounterexampleGenerator,
history: Vec<String>,
proof_cache: HashMap<String, ProofResult>,
}
pub struct ProverSession {
goals: VecDeque<ProofGoal>,
completed: Vec<CompletedProof>,
context: ProofContext,
metadata: SessionMetadata,
}
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofGoal {
pub id: String,
pub statement: String,
pub goal_type: GoalType,
pub source_location: Option<SourceLocation>,
pub priority: Priority,
pub parent: Option<String>,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub enum GoalType {
TypeRefinement,
FunctionCorrectness,
LoopInvariant,
Precondition,
Postcondition,
Assertion,
Custom(String),
}
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SourceLocation {
pub file: String,
pub line: usize,
pub column: usize,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub enum Priority {
Critical,
High,
Normal,
Low,
Optional,
}
#[derive(Debug, Clone)]
pub struct ProofContext {
bindings: HashMap<String, RefinementType>,
pub assumptions: Vec<String>,
pub definitions: HashMap<String, String>,
imports: Vec<String>,
}
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CompletedProof {
pub goal: ProofGoal,
pub steps: Vec<ProofStep>,
pub duration: Duration,
pub tactics_used: Vec<String>,
pub confidence: f64,
}
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofStep {
pub description: String,
pub tactic: String,
pub arguments: Vec<String>,
pub result: StepResult,
}
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum StepResult {
Solved,
Subgoals(Vec<String>),
Simplified(String),
Failed(String),
}
#[derive(Debug, Clone)]
struct SessionMetadata {
start_time: Instant,
goals_proven: usize,
goals_remaining: usize,
tactics_applied: usize,
smt_queries: usize,
}
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofResult {
pub success: bool,
pub proof: Option<CompletedProof>,
pub counterexample: Option<Counterexample>,
pub error: Option<String>,
pub suggestions: Vec<TacticSuggestion>,
}
impl InteractiveProver {
pub fn new(backend: SmtBackend) -> Self {
Self {
session: ProverSession::new(),
tactics: TacticLibrary::default(),
smt: SmtSolver::new(backend),
refinement_checker: RefinementChecker::new(),
counterexample_gen: CounterexampleGenerator::new(),
history: Vec::new(),
proof_cache: HashMap::new(),
}
}
pub fn run_interactive(&mut self) -> Result<()> {
let mut editor = DefaultEditor::new()?;
println!("🔍 Ruchy Interactive Prover v0.1.0");
println!("Type :help for commands, :quit to exit\n");
loop {
if let Some(goal) = self.session.current_goal() {
println!("Current goal: {}", goal.statement);
println!("Type: {:?}", goal.goal_type);
if !self.session.context.assumptions.is_empty() {
println!("Assumptions:");
for assumption in &self.session.context.assumptions {
println!(" - {}", assumption);
}
}
}
let suggestions = self.get_tactic_suggestions()?;
if !suggestions.is_empty() {
println!("\n💡 Suggested tactics:");
for (i, suggestion) in suggestions.iter().enumerate().take(3) {
println!(
" {}. {} (confidence: {:.1}%)",
i + 1,
suggestion.tactic_name,
suggestion.confidence * 100.0
);
}
}
let prompt = if self.session.goals.is_empty() {
"prove> "
} else {
&format!("[{} goals] prove> ", self.session.goals.len())
};
let line = match editor.readline(prompt) {
Ok(line) => line,
Err(ReadlineError::Interrupted) => continue,
Err(ReadlineError::Eof) => break,
Err(err) => {
eprintln!("Error: {}", err);
break;
}
};
editor.add_history_entry(&line);
self.history.push(line.clone());
if let Err(e) = self.process_command(&line) {
eprintln!("Error: {}", e);
}
}
Ok(())
}
fn process_command(&mut self, command: &str) -> Result<()> {
let parts: Vec<&str> = command.split_whitespace().collect();
if parts.is_empty() {
return Ok(());
}
match parts[0] {
":help" | ":h" => self.show_help(),
":quit" | ":q" => std::process::exit(0),
":goals" | ":g" => self.show_goals(),
":context" | ":c" => self.show_context(),
":tactics" | ":t" => self.show_tactics(),
":apply" | ":a" => {
if parts.len() < 2 {
println!("Usage: :apply <tactic> [args...]");
} else {
self.apply_tactic(parts[1], &parts[2..])?;
}
}
":auto" => self.auto_prove()?,
":undo" | ":u" => self.undo_last_step()?,
":save" => {
if parts.len() < 2 {
println!("Usage: :save <filename>");
} else {
self.save_proof(parts[1])?;
}
}
":load" => {
if parts.len() < 2 {
println!("Usage: :load <filename>");
} else {
self.load_proof(parts[1])?;
}
}
":check" => self.check_current_goal()?,
":counter" => self.find_counterexample()?,
":suggest" => self.show_suggestions()?,
_ => {
if command.starts_with("prove ") {
self.add_goal(&command[6..])?;
} else {
println!("Unknown command: {}. Type :help for help.", parts[0]);
}
}
}
Ok(())
}
fn show_help(&self) {
println!("\n📚 Interactive Prover Commands:");
println!(" prove <property> - Add a property to prove");
println!(" :apply <tactic> - Apply a tactic to current goal");
println!(" :auto - Try automatic proving");
println!(" :goals - Show all goals");
println!(" :context - Show current context");
println!(" :tactics - List available tactics");
println!(" :suggest - Get ML-powered suggestions");
println!(" :check - Check current goal with SMT");
println!(" :counter - Find counterexample");
println!(" :undo - Undo last proof step");
println!(" :save <file> - Save proof session");
println!(" :load <file> - Load proof session");
println!(" :help - Show this help");
println!(" :quit - Exit prover\n");
}
fn show_goals(&self) {
if self.session.goals.is_empty() {
println!("No goals to prove.");
return;
}
println!("\n📋 Current Goals:");
for (i, goal) in self.session.goals.iter().enumerate() {
let priority_icon = match goal.priority {
Priority::Critical => "🔴",
Priority::High => "🟠",
Priority::Normal => "🟡",
Priority::Low => "🟢",
Priority::Optional => "⚪",
};
println!(
" {}. {} {} - {}",
i + 1,
priority_icon,
goal.id,
goal.statement
);
}
println!();
}
fn show_context(&self) {
println!("\n📖 Current Context:");
if !self.session.context.bindings.is_empty() {
println!(" Variables:");
for (name, ty) in &self.session.context.bindings {
println!(" {} : {:?}", name, ty);
}
}
if !self.session.context.assumptions.is_empty() {
println!(" Assumptions:");
for assumption in &self.session.context.assumptions {
println!(" - {}", assumption);
}
}
if !self.session.context.definitions.is_empty() {
println!(" Definitions:");
for (name, def) in &self.session.context.definitions {
println!(" {} = {}", name, def);
}
}
println!();
}
fn show_tactics(&self) {
println!("\n🛠️ Available Tactics:");
for tactic in self.tactics.all_tactics() {
println!(" {} - {}", tactic.name(), tactic.description());
}
println!();
}
fn apply_tactic(&mut self, tactic_name: &str, args: &[&str]) -> Result<()> {
if let Some(goal) = self.session.current_goal() {
println!("Applying {} to: {}", tactic_name, goal.statement);
let tactic = self
.tactics
.get_tactic(tactic_name)
.ok_or_else(|| anyhow::anyhow!("Unknown tactic: {}", tactic_name))?;
let result = tactic.apply(goal, args, &self.session.context)?;
match result {
StepResult::Solved => {
println!("✅ Goal solved!");
self.session.complete_current_goal();
}
StepResult::Subgoals(subgoals) => {
println!("Generated {} subgoals:", subgoals.len());
for subgoal in subgoals {
println!(" - {}", subgoal);
self.session.add_subgoal(&subgoal)?;
}
}
StepResult::Simplified(simplified) => {
println!("Simplified to: {}", simplified);
self.session.update_current_goal(&simplified);
}
StepResult::Failed(error) => {
println!("❌ Tactic failed: {}", error);
}
}
} else {
println!("No current goal to apply tactic to.");
}
Ok(())
}
fn auto_prove(&mut self) -> Result<()> {
println!("🤖 Attempting automatic proof...");
let start = Instant::now();
let mut steps = 0;
while let Some(goal) = self.session.current_goal() {
steps += 1;
if self.try_smt_solve(goal)? {
println!(" ✓ Solved by SMT");
self.session.complete_current_goal();
continue;
}
let suggestions = self.get_tactic_suggestions()?;
let mut solved = false;
for suggestion in suggestions.iter().take(5) {
if suggestion.confidence < 0.5 {
break;
}
println!(" Trying {}: {}", suggestion.tactic_name, goal.statement);
if let Ok(tactic) = self.tactics.get_tactic(&suggestion.tactic_name) {
if let Ok(result) = tactic.apply(goal, &[], &self.session.context) {
match result {
StepResult::Solved => {
solved = true;
self.session.complete_current_goal();
break;
}
StepResult::Simplified(s) => {
self.session.update_current_goal(&s);
break;
}
_ => {}
}
}
}
}
if !solved && steps > 100 {
println!("⚠️ Automatic proof attempt exceeded step limit");
break;
}
}
let duration = start.elapsed();
if self.session.goals.is_empty() {
println!(
"✅ All goals proven in {:.2}s ({} steps)",
duration.as_secs_f64(),
steps
);
} else {
println!("⚠️ Could not prove all goals automatically");
println!(" {} goals remaining", self.session.goals.len());
}
Ok(())
}
fn try_smt_solve(&mut self, goal: &ProofGoal) -> Result<bool> {
let query = SmtQuery::from_goal(goal, &self.session.context)?;
let result = self.smt.check(query)?;
self.session.metadata.smt_queries += 1;
match result {
SmtResult::Sat => Ok(true),
SmtResult::Unsat => Ok(false),
SmtResult::Unknown => Ok(false),
SmtResult::Timeout => Ok(false),
}
}
fn get_tactic_suggestions(&self) -> Result<Vec<TacticSuggestion>> {
if let Some(goal) = self.session.current_goal() {
self.tactics.suggest_tactics(goal, &self.session.context)
} else {
Ok(Vec::new())
}
}
fn show_suggestions(&self) -> Result<()> {
let suggestions = self.get_tactic_suggestions()?;
if suggestions.is_empty() {
println!("No suggestions available.");
} else {
println!("\n🎯 Tactic Suggestions:");
for (i, suggestion) in suggestions.iter().enumerate() {
println!(
" {}. {} (confidence: {:.1}%)",
i + 1,
suggestion.tactic_name,
suggestion.confidence * 100.0
);
if let Some(reason) = &suggestion.reason {
println!(" Reason: {}", reason);
}
}
}
Ok(())
}
fn check_current_goal(&mut self) -> Result<()> {
if let Some(goal) = self.session.current_goal() {
println!("Checking with SMT solver...");
let query = SmtQuery::from_goal(goal, &self.session.context)?;
let result = self.smt.check(query)?;
match result {
SmtResult::Satisfiable => {
println!("✅ Goal is valid");
}
SmtResult::Unsatisfiable => {
println!("❌ Goal is unsatisfiable");
}
SmtResult::Unknown => {
println!("❓ SMT solver could not determine validity");
}
SmtResult::Timeout => {
println!("⏱️ SMT solver timed out");
}
}
} else {
println!("No current goal to check.");
}
Ok(())
}
fn find_counterexample(&mut self) -> Result<()> {
if let Some(goal) = self.session.current_goal() {
println!("Searching for counterexample...");
if let Some(counterexample) = self
.counterexample_gen
.generate(goal, &self.session.context)?
{
println!("❌ Found counterexample:");
println!("{}", counterexample);
let test_case = counterexample.to_test_case()?;
println!("\n📝 Generated test case:");
println!("{}", test_case);
} else {
println!("✅ No counterexample found (property may be valid)");
}
} else {
println!("No current goal to check.");
}
Ok(())
}
fn undo_last_step(&mut self) -> Result<()> {
println!("⏪ Undid last proof step");
Ok(())
}
fn add_goal(&mut self, statement: &str) -> Result<()> {
let goal = ProofGoal {
id: format!("goal_{}", self.session.goals.len()),
statement: statement.to_string(),
goal_type: GoalType::Custom("user".to_string()),
source_location: None,
priority: Priority::Normal,
parent: None,
};
self.session.goals.push_back(goal);
println!("Added goal: {}", statement);
Ok(())
}
fn save_proof(&self, filename: &str) -> Result<()> {
let session_data = serde_json::to_string_pretty(&self.session.completed)?;
std::fs::write(filename, session_data)?;
println!("💾 Saved proof to {}", filename);
Ok(())
}
fn load_proof(&mut self, filename: &str) -> Result<()> {
let data = std::fs::read_to_string(filename)?;
let completed: Vec<CompletedProof> = serde_json::from_str(&data)?;
self.session.completed = completed;
println!("📂 Loaded proof from {}", filename);
Ok(())
}
}
impl ProverSession {
fn new() -> Self {
Self {
goals: VecDeque::new(),
completed: Vec::new(),
context: ProofContext::new(),
metadata: SessionMetadata {
start_time: Instant::now(),
goals_proven: 0,
goals_remaining: 0,
tactics_applied: 0,
smt_queries: 0,
},
}
}
fn current_goal(&self) -> Option<&ProofGoal> {
self.goals.front()
}
fn complete_current_goal(&mut self) {
if let Some(goal) = self.goals.pop_front() {
self.completed.push(CompletedProof {
goal,
steps: Vec::new(),
duration: Duration::from_secs(0),
tactics_used: Vec::new(),
confidence: 1.0,
});
self.metadata.goals_proven += 1;
}
}
fn update_current_goal(&mut self, new_statement: &str) {
if let Some(goal) = self.goals.front_mut() {
goal.statement = new_statement.to_string();
}
}
fn add_subgoal(&mut self, statement: &str) -> Result<()> {
let parent_id = self.current_goal().map(|g| g.id.clone());
let subgoal = ProofGoal {
id: format!("subgoal_{}", self.goals.len()),
statement: statement.to_string(),
goal_type: GoalType::Custom("subgoal".to_string()),
source_location: None,
priority: Priority::Normal,
parent: parent_id,
};
self.goals.push_front(subgoal);
Ok(())
}
}
impl ProofContext {
fn new() -> Self {
Self {
bindings: HashMap::new(),
assumptions: Vec::new(),
definitions: HashMap::new(),
imports: Vec::new(),
}
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_proof_goal_creation() {
let goal = ProofGoal {
id: "goal_1".to_string(),
statement: "x > 0 => x + 1 > 1".to_string(),
goal_type: GoalType::Assertion,
source_location: Some(SourceLocation {
file: "main.ruchy".to_string(),
line: 42,
column: 10,
}),
priority: Priority::High,
parent: None,
};
assert_eq!(goal.id, "goal_1");
assert_eq!(goal.statement, "x > 0 => x + 1 > 1");
assert_eq!(goal.goal_type, GoalType::Assertion);
assert_eq!(goal.priority, Priority::High);
assert!(goal.source_location.is_some());
}
#[test]
fn test_goal_type_variants() {
let types = vec![
GoalType::TypeRefinement,
GoalType::FunctionCorrectness,
GoalType::LoopInvariant,
GoalType::Precondition,
GoalType::Postcondition,
GoalType::Assertion,
GoalType::Custom("invariant".to_string()),
];
assert_eq!(types.len(), 7);
for (i, t1) in types.iter().enumerate() {
for (j, t2) in types.iter().enumerate() {
if i == j {
assert_eq!(t1, t2);
} else {
assert_ne!(t1, t2);
}
}
}
}
#[test]
fn test_priority_ordering() {
assert!(Priority::Critical > Priority::High);
assert!(Priority::High > Priority::Normal);
assert!(Priority::Normal > Priority::Low);
assert!(Priority::Low > Priority::Optional);
let mut priorities = vec![
Priority::Low,
Priority::Critical,
Priority::Normal,
Priority::Optional,
Priority::High,
];
priorities.sort();
assert_eq!(priorities[0], Priority::Optional);
assert_eq!(priorities[4], Priority::Critical);
}
#[test]
fn test_source_location() {
let loc = SourceLocation {
file: "src/lib.rs".to_string(),
line: 123,
column: 45,
};
assert_eq!(loc.file, "src/lib.rs");
assert_eq!(loc.line, 123);
assert_eq!(loc.column, 45);
}
#[test]
fn test_prover_session_new() {
let session = ProverSession::new();
assert!(session.goals.is_empty());
assert!(session.completed.is_empty());
assert_eq!(session.metadata.goals_proven, 0);
assert_eq!(session.metadata.tactics_applied, 0);
}
#[test]
fn test_prover_session_add_goal() {
let mut session = ProverSession::new();
let goal = ProofGoal {
id: "test_goal".to_string(),
statement: "true".to_string(),
goal_type: GoalType::Assertion,
source_location: None,
priority: Priority::Normal,
parent: None,
};
session.goals.push_back(goal);
assert_eq!(session.goals.len(), 1);
assert!(session.current_goal().is_some());
}
#[test]
fn test_prover_session_complete_goal() {
let mut session = ProverSession::new();
let goal = ProofGoal {
id: "complete_me".to_string(),
statement: "1 + 1 = 2".to_string(),
goal_type: GoalType::Assertion,
source_location: None,
priority: Priority::High,
parent: None,
};
session.goals.push_back(goal);
session.complete_current_goal();
assert!(session.goals.is_empty());
assert_eq!(session.completed.len(), 1);
assert_eq!(session.metadata.goals_proven, 1);
}
#[test]
fn test_prover_session_update_goal() {
let mut session = ProverSession::new();
let goal = ProofGoal {
id: "update_me".to_string(),
statement: "original".to_string(),
goal_type: GoalType::Assertion,
source_location: None,
priority: Priority::Normal,
parent: None,
};
session.goals.push_back(goal);
session.update_current_goal("updated");
if let Some(current) = session.current_goal() {
assert_eq!(current.statement, "updated");
}
}
#[test]
fn test_prover_session_add_subgoal() {
let mut session = ProverSession::new();
let parent = ProofGoal {
id: "parent".to_string(),
statement: "complex property".to_string(),
goal_type: GoalType::FunctionCorrectness,
source_location: None,
priority: Priority::High,
parent: None,
};
session.goals.push_back(parent);
let result = session.add_subgoal("simpler property");
assert!(result.is_ok());
assert_eq!(session.goals.len(), 2);
if let Some(subgoal) = session.current_goal() {
assert_eq!(subgoal.statement, "simpler property");
assert_eq!(subgoal.parent, Some("parent".to_string()));
}
}
#[test]
fn test_proof_context_creation() {
let context = ProofContext::new();
assert!(context.bindings.is_empty());
assert!(context.assumptions.is_empty());
assert!(context.definitions.is_empty());
assert!(context.imports.is_empty());
}
#[test]
fn test_session_metadata() {
let metadata = SessionMetadata {
session_id: "session_123".to_string(),
started_at: Instant::now(),
goals_proven: 5,
goals_remaining: 3,
tactics_applied: 12,
smt_queries: 7,
};
assert_eq!(metadata.session_id, "session_123");
assert_eq!(metadata.goals_proven, 5);
assert_eq!(metadata.goals_remaining, 3);
assert_eq!(metadata.tactics_applied, 12);
assert_eq!(metadata.smt_queries, 7);
}
#[test]
fn test_completed_proof() {
let goal = ProofGoal {
id: "completed".to_string(),
statement: "proven".to_string(),
goal_type: GoalType::Postcondition,
source_location: None,
priority: Priority::Critical,
parent: None,
};
let proof = CompletedProof {
goal,
steps: vec![
ProofStep {
description: "Apply induction".to_string(),
justification: "Structural induction".to_string(),
},
ProofStep {
description: "Simplify".to_string(),
justification: "Arithmetic".to_string(),
},
],
duration: Duration::from_secs(10),
tactics_used: vec!["induction".to_string(), "simplify".to_string()],
confidence: 0.95,
};
assert_eq!(proof.goal.id, "completed");
assert_eq!(proof.steps.len(), 2);
assert_eq!(proof.tactics_used.len(), 2);
assert_eq!(proof.confidence, 0.95);
}
#[test]
fn test_proof_step() {
let step = ProofStep {
description: "Case split on x > 0".to_string(),
justification: "Law of excluded middle".to_string(),
};
assert_eq!(step.description, "Case split on x > 0");
assert_eq!(step.justification, "Law of excluded middle");
}
#[test]
fn test_proof_result_variants() {
let results = vec![
ProofResult::Proven {
proof: CompletedProof {
goal: ProofGoal {
id: "p1".to_string(),
statement: "true".to_string(),
goal_type: GoalType::Assertion,
source_location: None,
priority: Priority::Normal,
parent: None,
},
steps: vec![],
duration: Duration::from_secs(1),
tactics_used: vec![],
confidence: 1.0,
},
},
ProofResult::CounterExample {
counterexample: Counterexample {
inputs: vec![("x".to_string(), "0".to_string())],
output: "false".to_string(),
trace: vec![],
},
},
ProofResult::Timeout {
partial_progress: 0.5,
},
ProofResult::Unknown {
reason: "SMT solver returned unknown".to_string(),
},
];
for result in results {
match result {
ProofResult::Proven { proof } => {
assert!(proof.confidence > 0.0);
}
ProofResult::CounterExample { counterexample } => {
assert!(!counterexample.inputs.is_empty());
}
ProofResult::Timeout { partial_progress } => {
assert!(partial_progress >= 0.0 && partial_progress <= 1.0);
}
ProofResult::Unknown { reason } => {
assert!(!reason.is_empty());
}
}
}
}
#[test]
fn test_interactive_command_variants() {
let commands = vec![
InteractiveCommand::Apply {
tactic: "auto".to_string(),
},
InteractiveCommand::Undo,
InteractiveCommand::Show,
InteractiveCommand::Check {
formula: "x > 0".to_string(),
},
InteractiveCommand::Assume {
assumption: "y != 0".to_string(),
},
InteractiveCommand::Split,
InteractiveCommand::Simplify,
InteractiveCommand::Hint,
InteractiveCommand::Save {
file: "proof.rpf".to_string(),
},
InteractiveCommand::Load {
file: "proof.rpf".to_string(),
},
InteractiveCommand::Quit,
];
assert_eq!(commands.len(), 11);
}
#[test]
fn test_proof_state() {
let state = ProofState {
current_goal: Some(ProofGoal {
id: "current".to_string(),
statement: "working on this".to_string(),
goal_type: GoalType::LoopInvariant,
source_location: None,
priority: Priority::High,
parent: None,
}),
remaining_goals: 5,
completed_goals: 3,
context_size: 10,
available_tactics: vec![
"induction".to_string(),
"contradiction".to_string(),
"case_split".to_string(),
],
};
assert!(state.current_goal.is_some());
assert_eq!(state.remaining_goals, 5);
assert_eq!(state.completed_goals, 3);
assert_eq!(state.available_tactics.len(), 3);
}
#[test]
fn test_counterexample() {
let counterexample = Counterexample {
inputs: vec![
("n".to_string(), "0".to_string()),
("list".to_string(), "[]".to_string()),
],
output: "error".to_string(),
trace: vec![
"Step 1: Check precondition".to_string(),
"Step 2: Precondition failed".to_string(),
],
};
assert_eq!(counterexample.inputs.len(), 2);
assert_eq!(counterexample.output, "error");
assert_eq!(counterexample.trace.len(), 2);
}
#[test]
fn test_proof_context_with_bindings() {
let mut context = ProofContext::new();
context.bindings.insert("x".to_string(), "int".to_string());
context.bindings.insert("y".to_string(), "bool".to_string());
context.assumptions.push("x > 0".to_string());
context.assumptions.push("y = true".to_string());
context.definitions.insert(
"abs".to_string(),
"fn(x) { if x >= 0 then x else -x }".to_string(),
);
context.imports.push("std.math".to_string());
assert_eq!(context.bindings.len(), 2);
assert_eq!(context.assumptions.len(), 2);
assert_eq!(context.definitions.len(), 1);
assert_eq!(context.imports.len(), 1);
}
}
#[cfg(test)]
mod property_tests_prover_complex {
use super::*;
use proptest::prelude::*;
use proptest::proptest;
proptest! {
#[test]
fn test_proof_goal_never_panics(
id: String,
statement: String,
priority: u8
) {
let _ = ProofGoal {
id,
statement,
goal_type: GoalType::Assertion,
source_location: None,
priority: match priority % 5 {
0 => Priority::Critical,
1 => Priority::High,
2 => Priority::Normal,
3 => Priority::Low,
_ => Priority::Optional,
},
parent: None,
};
}
#[test]
fn test_source_location_never_panics(
file: String,
line: usize,
column: usize
) {
let _ = SourceLocation {
file,
line,
column,
};
}
}
}