Skip to main content

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/// Parse a goal string like `ancestor(X, bob)` into a `Predicate`.
13///
14/// Returns an error with a descriptive message if the string is malformed.
15fn parse_goal(goal: &str) -> Result<ipfrs::Predicate> {
16    use ipfrs::{Constant, Predicate, Term};
17
18    let goal = goal.trim();
19    let paren_open = goal.find('(').ok_or_else(|| {
20        anyhow::anyhow!(
21            "Invalid goal '{}': expected 'predicate(args...)' syntax",
22            goal
23        )
24    })?;
25    let paren_close = goal
26        .rfind(')')
27        .ok_or_else(|| anyhow::anyhow!("Invalid goal '{}': missing closing ')'", goal))?;
28
29    if paren_close <= paren_open {
30        return Err(anyhow::anyhow!(
31            "Invalid goal '{}': closing ')' appears before or at '('",
32            goal
33        ));
34    }
35
36    let predicate_name = goal[..paren_open].trim().to_string();
37    if predicate_name.is_empty() {
38        return Err(anyhow::anyhow!(
39            "Invalid goal '{}': predicate name is empty",
40            goal
41        ));
42    }
43
44    let args_str = &goal[paren_open + 1..paren_close];
45    let mut terms = Vec::new();
46
47    for raw in args_str.split(',') {
48        let token = raw.trim();
49        if token.is_empty() {
50            continue;
51        }
52        let term = if token.starts_with('"') && token.ends_with('"') {
53            let s = token.trim_matches('"');
54            Term::Const(Constant::String(s.to_string()))
55        } else if let Ok(n) = token.parse::<i64>() {
56            Term::Const(Constant::Int(n))
57        } else if token.starts_with('?')
58            || token
59                .chars()
60                .next()
61                .map(|c| c.is_uppercase())
62                .unwrap_or(false)
63        {
64            Term::Var(token.to_string())
65        } else {
66            // Treat bare atoms as string constants
67            Term::Const(Constant::String(token.to_string()))
68        };
69        terms.push(term);
70    }
71
72    Ok(Predicate::new(predicate_name, terms))
73}
74
75/// Logic Datalog-style query with streaming output and indicatif spinner.
76///
77/// Identical to [`logic_query`] in terms of logic execution, but shows a
78/// "Searching…" spinner on TTY while inference is running, then prints each
79/// result binding as it arrives.  JSON output uses newline-delimited records.
80pub async fn logic_query_streaming(
81    goal: &str,
82    max_depth: usize,
83    json_output: bool,
84    timeout_secs: u64,
85) -> Result<()> {
86    use ipfrs::{Node, NodeConfig};
87    use std::time::Instant;
88
89    let goal_pred = parse_goal(goal)?;
90
91    let mut node = Node::new(NodeConfig::default().with_tensorlogic())?;
92    node.start().await?;
93
94    // Show a spinner while inference runs — hidden on non-TTY automatically
95    // because indicatif ProgressBar uses atty detection internally.
96    let spinner = {
97        use indicatif::{ProgressBar, ProgressStyle};
98        use std::time::Duration;
99        let pb = ProgressBar::new_spinner();
100        pb.set_style(
101            ProgressStyle::default_spinner()
102                .template("{spinner:.cyan} {msg}")
103                .unwrap_or_else(|_| ProgressStyle::default_spinner()),
104        );
105        pb.set_message("Searching...");
106        pb.enable_steady_tick(Duration::from_millis(80));
107        pb
108    };
109
110    let start = Instant::now();
111
112    let solutions = match tokio::time::timeout(
113        std::time::Duration::from_secs(timeout_secs),
114        async { node.infer(&goal_pred) },
115    )
116    .await
117    {
118        Ok(Ok(s)) => s,
119        Ok(Err(_)) => {
120            spinner.finish_and_clear();
121            crate::output::warning(
122                "TensorLogic not initialized. Use 'ipfrs logic' commands to load a knowledge base first.",
123            );
124            node.stop().await?;
125            if json_output {
126                println!(
127                    "{{\"goal\": \"{}\", \"proved\": false, \"solutions\": [], \"time_ms\": 0}}",
128                    goal
129                );
130            } else {
131                println!("Logic query: {}", goal);
132                println!("Proved: No");
133                println!();
134                println!("Bindings:");
135                println!("  (none)");
136                println!();
137                println!("Time: 0ms | Depth: {}", max_depth);
138            }
139            return Ok(());
140        }
141        Err(_) => {
142            spinner.finish_and_clear();
143            node.stop().await?;
144            return Err(anyhow::anyhow!(
145                "Logic query timed out after {} seconds",
146                timeout_secs
147            ));
148        }
149    };
150
151    let elapsed_ms = start.elapsed().as_millis();
152    spinner.finish_and_clear();
153    node.stop().await?;
154
155    let proved = !solutions.is_empty();
156
157    if json_output {
158        // Newline-delimited JSON — emit header record then one record per solution.
159        println!(
160            "{{\"goal\": \"{}\", \"proved\": {}, \"time_ms\": {}}}",
161            goal, proved, elapsed_ms
162        );
163        for solution in &solutions {
164            let binding_pairs: Vec<String> = solution
165                .iter()
166                .map(|(var, term)| format!("\"{}\": \"{}\"", var, term))
167                .collect();
168            println!("{{{}}}", binding_pairs.join(", "));
169        }
170    } else {
171        println!("Logic query: {}", goal);
172        println!("Proved: {}", if proved { "Yes" } else { "No" });
173        println!();
174        println!("Bindings:");
175        if solutions.is_empty() {
176            println!("  (none)");
177        } else {
178            // Stream each solution as it would arrive.
179            for (i, solution) in solutions.iter().enumerate() {
180                let bindings: Vec<String> = solution
181                    .iter()
182                    .map(|(var, term)| format!("{} = {}", var, term))
183                    .collect();
184                println!("  Solution {}: {}", i + 1, bindings.join(", "));
185            }
186        }
187        println!();
188        println!("Time: {}ms | Depth: {}", elapsed_ms, max_depth);
189    }
190
191    Ok(())
192}
193
194/// Filter an explicit list of CIDs through the logic engine.
195///
196/// This is the programmatic counterpart to [`logic_filter`], accepting an
197/// already-collected `Vec<String>` of CIDs instead of reading from stdin.
198/// Used by the hybrid pipeline to apply a logic predicate to semantic results.
199pub async fn logic_filter_cids(
200    cids: &[String],
201    predicate_template: &str,
202    json_output: bool,
203) -> Result<()> {
204    use ipfrs::{Node, NodeConfig};
205
206    if cids.is_empty() {
207        if json_output {
208            println!("[]");
209        }
210        return Ok(());
211    }
212
213    let mut node = Node::new(NodeConfig::default().with_tensorlogic())?;
214    node.start().await?;
215
216    let mut matched_cids: Vec<String> = Vec::new();
217
218    for cid in cids {
219        let goal_str = predicate_template.replace('X', cid);
220        let goal_pred = match parse_goal(&goal_str) {
221            Ok(p) => p,
222            Err(e) => {
223                crate::output::warning(&format!("Skipping CID {}: {}", cid, e));
224                continue;
225            }
226        };
227        let solutions = node.infer(&goal_pred).unwrap_or_default();
228        if !solutions.is_empty() {
229            matched_cids.push(cid.clone());
230        }
231    }
232
233    node.stop().await.ok();
234
235    if json_output {
236        let json_items: Vec<String> = matched_cids.iter().map(|c| format!("\"{}\"", c)).collect();
237        println!("[{}]", json_items.join(", "));
238    } else {
239        if matched_cids.is_empty() {
240            println!("  (no CIDs matched predicate: {})", predicate_template);
241        } else {
242            for cid in &matched_cids {
243                println!("  {}", cid);
244            }
245        }
246    }
247
248    Ok(())
249}
250
251/// Logic Datalog-style query: `ipfrs logic query "ancestor(X, bob)"`
252pub async fn logic_query(
253    goal: &str,
254    max_depth: usize,
255    json_output: bool,
256    timeout_secs: u64,
257) -> Result<()> {
258    use ipfrs::{Node, NodeConfig};
259    use std::time::Instant;
260
261    let goal_pred = parse_goal(goal)?;
262
263    let mut node = Node::new(NodeConfig::default().with_tensorlogic())?;
264    node.start().await?;
265
266    let start = Instant::now();
267
268    let solutions = match tokio::time::timeout(
269        std::time::Duration::from_secs(timeout_secs),
270        async { node.infer(&goal_pred) },
271    )
272    .await
273    {
274        Ok(Ok(s)) => s,
275        Ok(Err(_)) => {
276            crate::output::warning(
277                "TensorLogic not initialized. Use 'ipfrs logic' commands to load a knowledge base first.",
278            );
279            node.stop().await?;
280            if json_output {
281                println!(
282                    "{{\"goal\": \"{}\", \"proved\": false, \"solutions\": [], \"time_ms\": 0}}",
283                    goal
284                );
285            } else {
286                println!("Logic query: {}", goal);
287                println!("Proved: No");
288                println!();
289                println!("Bindings:");
290                println!("  (none)");
291                println!();
292                println!("Time: 0ms | Depth: {}", max_depth);
293            }
294            return Ok(());
295        }
296        Err(_) => {
297            node.stop().await?;
298            return Err(anyhow::anyhow!(
299                "Logic query timed out after {} seconds",
300                timeout_secs
301            ));
302        }
303    };
304
305    let elapsed_ms = start.elapsed().as_millis();
306    node.stop().await?;
307
308    let proved = !solutions.is_empty();
309
310    if json_output {
311        println!("{{");
312        println!("  \"goal\": \"{}\",", goal);
313        println!("  \"proved\": {},", proved);
314        println!("  \"solutions\": [");
315        for (i, solution) in solutions.iter().enumerate() {
316            let comma = if i + 1 < solutions.len() { "," } else { "" };
317            let binding_pairs: Vec<String> = solution
318                .iter()
319                .map(|(var, term)| format!("\"{}\": \"{}\"", var, term))
320                .collect();
321            println!("    {{{}}} {}", binding_pairs.join(", "), comma);
322        }
323        println!("  ],");
324        println!("  \"time_ms\": {}", elapsed_ms);
325        println!("}}");
326    } else {
327        println!("Logic query: {}", goal);
328        println!("Proved: {}", if proved { "Yes" } else { "No" });
329        println!();
330        println!("Bindings:");
331        if solutions.is_empty() {
332            println!("  (none)");
333        } else {
334            for (i, solution) in solutions.iter().enumerate() {
335                let bindings: Vec<String> = solution
336                    .iter()
337                    .map(|(var, term)| format!("{} = {}", var, term))
338                    .collect();
339                println!("  Solution {}: {}", i + 1, bindings.join(", "));
340            }
341        }
342        println!();
343        println!("Time: {}ms | Depth: {}", elapsed_ms, max_depth);
344    }
345
346    Ok(())
347}
348
349/// Run inference query
350pub async fn logic_infer(predicate: &str, terms: &[String], format: &str) -> Result<()> {
351    use ipfrs::{Constant, Node, NodeConfig, Predicate, Term};
352
353    let mut node = Node::new(NodeConfig::default())?;
354    node.start().await?;
355
356    // Parse terms from JSON strings
357    let mut parsed_terms = Vec::new();
358    for term_str in terms {
359        if term_str.starts_with('"') && term_str.ends_with('"') {
360            // String constant
361            let s = term_str.trim_matches('"');
362            parsed_terms.push(Term::Const(Constant::String(s.to_string())));
363        } else if term_str.parse::<i64>().is_ok() {
364            // Integer constant
365            let n = term_str.parse::<i64>()?;
366            parsed_terms.push(Term::Const(Constant::Int(n)));
367        } else if term_str.starts_with('?')
368            || term_str
369                .chars()
370                .next()
371                .map(|c| c.is_uppercase())
372                .unwrap_or(false)
373        {
374            // Variable
375            parsed_terms.push(Term::Var(term_str.to_string()));
376        } else {
377            return Err(anyhow::anyhow!("Invalid term: {}", term_str));
378        }
379    }
380
381    let goal = Predicate::new(predicate.to_string(), parsed_terms);
382
383    println!("Running inference query: {}", goal);
384    let solutions = node.infer(&goal)?;
385
386    match format {
387        "json" => {
388            println!("{{");
389            println!("  \"goal\": \"{}\",", goal);
390            println!("  \"solutions\": [");
391            for (i, solution) in solutions.iter().enumerate() {
392                print!("    {{");
393                for (j, (var, term)) in solution.iter().enumerate() {
394                    print!("\"{}\": \"{}\"", var, term);
395                    if j < solution.len() - 1 {
396                        print!(", ");
397                    }
398                }
399                print!("}}");
400                if i < solutions.len() - 1 {
401                    println!(",");
402                } else {
403                    println!();
404                }
405            }
406            println!("  ]");
407            println!("}}");
408        }
409        _ => {
410            if solutions.is_empty() {
411                println!("No solutions found");
412            } else {
413                println!("Found {} solution(s):", solutions.len());
414                for (i, solution) in solutions.iter().enumerate() {
415                    println!("  Solution {}:", i + 1);
416                    for (var, term) in solution {
417                        println!("    {} = {}", var, term);
418                    }
419                }
420            }
421        }
422    }
423
424    node.stop().await?;
425    Ok(())
426}
427
428/// Generate proof for a goal
429pub async fn logic_prove(predicate: &str, terms: &[String], format: &str) -> Result<()> {
430    use ipfrs::{Constant, Node, NodeConfig, Predicate, Term};
431
432    let mut node = Node::new(NodeConfig::default())?;
433    node.start().await?;
434
435    // Parse terms from JSON strings (same as infer)
436    let mut parsed_terms = Vec::new();
437    for term_str in terms {
438        if term_str.starts_with('"') && term_str.ends_with('"') {
439            let s = term_str.trim_matches('"');
440            parsed_terms.push(Term::Const(Constant::String(s.to_string())));
441        } else if term_str.parse::<i64>().is_ok() {
442            let n = term_str.parse::<i64>()?;
443            parsed_terms.push(Term::Const(Constant::Int(n)));
444        } else if term_str.starts_with('?')
445            || term_str
446                .chars()
447                .next()
448                .map(|c| c.is_uppercase())
449                .unwrap_or(false)
450        {
451            parsed_terms.push(Term::Var(term_str.to_string()));
452        } else {
453            return Err(anyhow::anyhow!("Invalid term: {}", term_str));
454        }
455    }
456
457    let goal = Predicate::new(predicate.to_string(), parsed_terms);
458
459    println!("Generating proof for: {}", goal);
460    let proof = node.prove(&goal)?;
461
462    match format {
463        "json" => {
464            println!("{{");
465            println!("  \"goal\": \"{}\",", goal);
466            if let Some(p) = &proof {
467                println!("  \"proof_found\": true,");
468                println!("  \"proof\": {{");
469                println!("    \"goal\": \"{}\",", p.goal);
470                if let Some(rule) = &p.rule {
471                    println!("    \"is_fact\": {},", rule.is_fact);
472                    println!("    \"subproofs\": {}", p.subproofs.len());
473                } else {
474                    println!("    \"is_fact\": true,");
475                    println!("    \"subproofs\": 0");
476                }
477                println!("  }}");
478            } else {
479                println!("  \"proof_found\": false");
480            }
481            println!("}}");
482        }
483        _ => {
484            if let Some(p) = &proof {
485                println!("Proof found!");
486                println!("Goal: {}", p.goal);
487                if let Some(rule) = &p.rule {
488                    if rule.is_fact {
489                        println!("Proved by fact");
490                    } else {
491                        println!("Proved by rule: {} :- {:?}", rule.head, rule.body);
492                        println!("Number of subproofs: {}", p.subproofs.len());
493                    }
494                }
495            } else {
496                println!("No proof found");
497            }
498        }
499    }
500
501    node.stop().await?;
502    Ok(())
503}
504
505/// Show knowledge base statistics
506pub async fn logic_kb_stats(format: &str) -> Result<()> {
507    use ipfrs::{Node, NodeConfig};
508
509    let mut node = Node::new(NodeConfig::default())?;
510    node.start().await?;
511
512    let stats = node.kb_stats()?;
513
514    match format {
515        "json" => {
516            println!("{{");
517            println!("  \"num_facts\": {},", stats.num_facts);
518            println!("  \"num_rules\": {}", stats.num_rules);
519            println!("}}");
520        }
521        _ => {
522            println!("Knowledge Base Statistics");
523            println!("=========================");
524            println!("Facts: {}", stats.num_facts);
525            println!("Rules: {}", stats.num_rules);
526        }
527    }
528
529    node.stop().await?;
530    Ok(())
531}
532
533/// Save knowledge base to file
534pub async fn logic_kb_save(path: &str) -> Result<()> {
535    use ipfrs::{Node, NodeConfig};
536
537    let mut node = Node::new(NodeConfig::default())?;
538    node.start().await?;
539
540    println!("Saving knowledge base to {}...", path);
541    node.save_knowledge_base(path).await?;
542    println!("Knowledge base saved successfully");
543
544    node.stop().await?;
545    Ok(())
546}
547
548/// Load knowledge base from file
549pub async fn logic_kb_load(path: &str) -> Result<()> {
550    use ipfrs::{Node, NodeConfig};
551
552    let mut node = Node::new(NodeConfig::default())?;
553    node.start().await?;
554
555    println!("Loading knowledge base from {}...", path);
556    node.load_knowledge_base(path).await?;
557    println!("Knowledge base loaded successfully");
558
559    let stats = node.kb_stats()?;
560    println!(
561        "Loaded {} facts and {} rules",
562        stats.num_facts, stats.num_rules
563    );
564
565    node.stop().await?;
566    Ok(())
567}
568
569/// Read CIDs from stdin and filter by logic predicate.
570///
571/// Each non-empty line on stdin is treated as a CID. The predicate template
572/// uses `X` as a placeholder that is replaced by the CID before inference.
573///
574/// # Example
575/// ```text
576/// echo "bafkrei123" | ipfrs logic filter "indexed(X)"
577/// ```
578pub async fn logic_filter(
579    predicate_template: &str,
580    json_output: bool,
581    data_dir: &str,
582) -> Result<()> {
583    use ipfrs::{Node, NodeConfig};
584    use std::io::{self, BufRead};
585
586    let _ = data_dir; // reserved for future per-repo node config
587
588    let stdin = io::stdin();
589    let mut matched_cids: Vec<String> = Vec::new();
590
591    // Collect all CIDs first so we can start the node once.
592    let cids: Vec<String> = stdin
593        .lock()
594        .lines()
595        .filter_map(|line_result| line_result.ok().map(|l| l.trim().to_string()))
596        .filter(|l| !l.is_empty())
597        .collect();
598
599    if cids.is_empty() {
600        // Nothing on stdin — emit empty output and exit cleanly.
601        if json_output {
602            println!("[]");
603        }
604        return Ok(());
605    }
606
607    let mut node = Node::new(NodeConfig::default().with_tensorlogic())?;
608    node.start().await?;
609
610    for cid in &cids {
611        // Instantiate the predicate template: "valid(X)" -> "valid(bafkrei...)"
612        let goal_str = predicate_template.replace('X', cid);
613
614        let goal_pred = match parse_goal(&goal_str) {
615            Ok(p) => p,
616            Err(e) => {
617                crate::output::warning(&format!("Skipping CID {}: {}", cid, e));
618                continue;
619            }
620        };
621
622        let solutions = node.infer(&goal_pred).unwrap_or_default();
623        if !solutions.is_empty() {
624            matched_cids.push(cid.clone());
625        }
626    }
627
628    node.stop().await.ok();
629
630    if json_output {
631        let json_items: Vec<String> = matched_cids.iter().map(|c| format!("\"{}\"", c)).collect();
632        println!("[{}]", json_items.join(", "));
633    } else {
634        for cid in &matched_cids {
635            println!("{}", cid);
636        }
637    }
638
639    Ok(())
640}
641
642#[cfg(test)]
643mod filter_tests {
644    #[test]
645    fn test_predicate_instantiation() {
646        // "valid(X)" -> "valid(bafkrei123)"
647        let template = "valid(X)";
648        let cid = "bafkrei123";
649        let goal = template.replace('X', cid);
650        assert_eq!(goal, "valid(bafkrei123)");
651    }
652
653    #[test]
654    fn test_predicate_instantiation_multiple_vars() {
655        // "related(X, topic)" — X is substituted, other tokens untouched
656        let goal = "related(X, topic)".replace('X', "cid456");
657        assert_eq!(goal, "related(cid456, topic)");
658    }
659
660    #[test]
661    fn test_predicate_instantiation_no_placeholder() {
662        // Template without X is left unchanged
663        let goal = "indexed(item)".replace('X', "cid789");
664        assert_eq!(goal, "indexed(item)");
665    }
666}