ipfrs_cli/commands/
logic.rs

1//! Logic programming commands
2//!
3//! This module provides logic operations:
4//! - `logic_infer` - Run inference query
5//! - `logic_prove` - Generate proof
6//! - `logic_kb_stats` - Knowledge base statistics
7//! - `logic_kb_save` - Save knowledge base
8//! - `logic_kb_load` - Load knowledge base
9
10use anyhow::Result;
11
12/// Run inference query
13pub async fn logic_infer(predicate: &str, terms: &[String], format: &str) -> Result<()> {
14    use ipfrs::{Constant, Node, NodeConfig, Predicate, Term};
15
16    let mut node = Node::new(NodeConfig::default())?;
17    node.start().await?;
18
19    // Parse terms from JSON strings
20    let mut parsed_terms = Vec::new();
21    for term_str in terms {
22        if term_str.starts_with('"') && term_str.ends_with('"') {
23            // String constant
24            let s = term_str.trim_matches('"');
25            parsed_terms.push(Term::Const(Constant::String(s.to_string())));
26        } else if term_str.parse::<i64>().is_ok() {
27            // Integer constant
28            let n = term_str.parse::<i64>()?;
29            parsed_terms.push(Term::Const(Constant::Int(n)));
30        } else if term_str.starts_with('?') || term_str.chars().next().unwrap().is_uppercase() {
31            // Variable
32            parsed_terms.push(Term::Var(term_str.to_string()));
33        } else {
34            return Err(anyhow::anyhow!("Invalid term: {}", term_str));
35        }
36    }
37
38    let goal = Predicate::new(predicate.to_string(), parsed_terms);
39
40    println!("Running inference query: {}", goal);
41    let solutions = node.infer(&goal)?;
42
43    match format {
44        "json" => {
45            println!("{{");
46            println!("  \"goal\": \"{}\",", goal);
47            println!("  \"solutions\": [");
48            for (i, solution) in solutions.iter().enumerate() {
49                print!("    {{");
50                for (j, (var, term)) in solution.iter().enumerate() {
51                    print!("\"{}\": \"{}\"", var, term);
52                    if j < solution.len() - 1 {
53                        print!(", ");
54                    }
55                }
56                print!("}}");
57                if i < solutions.len() - 1 {
58                    println!(",");
59                } else {
60                    println!();
61                }
62            }
63            println!("  ]");
64            println!("}}");
65        }
66        _ => {
67            if solutions.is_empty() {
68                println!("No solutions found");
69            } else {
70                println!("Found {} solution(s):", solutions.len());
71                for (i, solution) in solutions.iter().enumerate() {
72                    println!("  Solution {}:", i + 1);
73                    for (var, term) in solution {
74                        println!("    {} = {}", var, term);
75                    }
76                }
77            }
78        }
79    }
80
81    node.stop().await?;
82    Ok(())
83}
84
85/// Generate proof for a goal
86pub async fn logic_prove(predicate: &str, terms: &[String], format: &str) -> Result<()> {
87    use ipfrs::{Constant, Node, NodeConfig, Predicate, Term};
88
89    let mut node = Node::new(NodeConfig::default())?;
90    node.start().await?;
91
92    // Parse terms from JSON strings (same as infer)
93    let mut parsed_terms = Vec::new();
94    for term_str in terms {
95        if term_str.starts_with('"') && term_str.ends_with('"') {
96            let s = term_str.trim_matches('"');
97            parsed_terms.push(Term::Const(Constant::String(s.to_string())));
98        } else if term_str.parse::<i64>().is_ok() {
99            let n = term_str.parse::<i64>()?;
100            parsed_terms.push(Term::Const(Constant::Int(n)));
101        } else if term_str.starts_with('?') || term_str.chars().next().unwrap().is_uppercase() {
102            parsed_terms.push(Term::Var(term_str.to_string()));
103        } else {
104            return Err(anyhow::anyhow!("Invalid term: {}", term_str));
105        }
106    }
107
108    let goal = Predicate::new(predicate.to_string(), parsed_terms);
109
110    println!("Generating proof for: {}", goal);
111    let proof = node.prove(&goal)?;
112
113    match format {
114        "json" => {
115            println!("{{");
116            println!("  \"goal\": \"{}\",", goal);
117            if let Some(p) = &proof {
118                println!("  \"proof_found\": true,");
119                println!("  \"proof\": {{");
120                println!("    \"goal\": \"{}\",", p.goal);
121                if let Some(rule) = &p.rule {
122                    println!("    \"is_fact\": {},", rule.is_fact);
123                    println!("    \"subproofs\": {}", p.subproofs.len());
124                } else {
125                    println!("    \"is_fact\": true,");
126                    println!("    \"subproofs\": 0");
127                }
128                println!("  }}");
129            } else {
130                println!("  \"proof_found\": false");
131            }
132            println!("}}");
133        }
134        _ => {
135            if let Some(p) = &proof {
136                println!("Proof found!");
137                println!("Goal: {}", p.goal);
138                if let Some(rule) = &p.rule {
139                    if rule.is_fact {
140                        println!("Proved by fact");
141                    } else {
142                        println!("Proved by rule: {} :- {:?}", rule.head, rule.body);
143                        println!("Number of subproofs: {}", p.subproofs.len());
144                    }
145                }
146            } else {
147                println!("No proof found");
148            }
149        }
150    }
151
152    node.stop().await?;
153    Ok(())
154}
155
156/// Show knowledge base statistics
157pub async fn logic_kb_stats(format: &str) -> Result<()> {
158    use ipfrs::{Node, NodeConfig};
159
160    let mut node = Node::new(NodeConfig::default())?;
161    node.start().await?;
162
163    let stats = node.kb_stats()?;
164
165    match format {
166        "json" => {
167            println!("{{");
168            println!("  \"num_facts\": {},", stats.num_facts);
169            println!("  \"num_rules\": {}", stats.num_rules);
170            println!("}}");
171        }
172        _ => {
173            println!("Knowledge Base Statistics");
174            println!("=========================");
175            println!("Facts: {}", stats.num_facts);
176            println!("Rules: {}", stats.num_rules);
177        }
178    }
179
180    node.stop().await?;
181    Ok(())
182}
183
184/// Save knowledge base to file
185pub async fn logic_kb_save(path: &str) -> Result<()> {
186    use ipfrs::{Node, NodeConfig};
187
188    let mut node = Node::new(NodeConfig::default())?;
189    node.start().await?;
190
191    println!("Saving knowledge base to {}...", path);
192    node.save_knowledge_base(path).await?;
193    println!("Knowledge base saved successfully");
194
195    node.stop().await?;
196    Ok(())
197}
198
199/// Load knowledge base from file
200pub async fn logic_kb_load(path: &str) -> Result<()> {
201    use ipfrs::{Node, NodeConfig};
202
203    let mut node = Node::new(NodeConfig::default())?;
204    node.start().await?;
205
206    println!("Loading knowledge base from {}...", path);
207    node.load_knowledge_base(path).await?;
208    println!("Knowledge base loaded successfully");
209
210    let stats = node.kb_stats()?;
211    println!(
212        "Loaded {} facts and {} rules",
213        stats.num_facts, stats.num_rules
214    );
215
216    node.stop().await?;
217    Ok(())
218}