use claimr::{Answer, ProofNode};
fn escape(s: &str) -> String {
let mut out = String::with_capacity(s.len() + 2);
for c in s.chars() {
match c {
'"' => out.push_str("\\\""),
'\\' => out.push_str("\\\\"),
'\n' => out.push_str("\\n"),
'\r' => out.push_str("\\r"),
'\t' => out.push_str("\\t"),
c if (c as u32) < 0x20 => out.push_str(&format!("\\u{:04x}", c as u32)),
c => out.push(c),
}
}
out
}
fn string_array(items: &[String]) -> String {
let inner: Vec<String> = items.iter().map(|s| format!("\"{}\"", escape(s))).collect();
format!("[{}]", inner.join(","))
}
fn answer_object(answer: &Answer) -> String {
let mut out = format!(
"{{\"equations\":{},\"disequations\":{},\"constraints\":{}",
string_array(&answer.equations),
string_array(&answer.disequations),
string_array(&answer.constraints),
);
if let Some(roots) = &answer.explanation {
out.push_str(",\"explanation\":");
out.push_str(&proof_array(roots));
}
out.push('}');
out
}
fn proof_array(roots: &[ProofNode]) -> String {
struct Open<'a> {
node: &'a ProofNode,
next_child: usize,
children: Vec<String>,
}
let mut rendered_roots: Vec<String> = Vec::new();
let mut stack: Vec<Open<'_>> = Vec::new();
let mut pending_roots = roots.iter();
loop {
let next = match stack.last_mut() {
Some(open) => {
let child = open.node.subgoals.get(open.next_child);
open.next_child += 1;
child
}
None => pending_roots.next(),
};
match next {
Some(node) => stack.push(Open {
node,
next_child: 0,
children: Vec::new(),
}),
None => {
let Some(done) = stack.pop() else {
break;
};
let text = proof_object(done.node, &done.children);
match stack.last_mut() {
Some(parent) => parent.children.push(text),
None => rendered_roots.push(text),
}
}
}
}
format!("[{}]", rendered_roots.join(","))
}
fn proof_object(node: &ProofNode, children: &[String]) -> String {
let mut fields = vec![
format!("\"goal\":\"{}\"", escape(&node.goal)),
format!("\"by\":\"{}\"", node.by.as_str()),
];
if let Some(line) = node.line {
fields.push(format!("\"line\":{line}"));
}
if let Some(column) = node.column {
fields.push(format!("\"column\":{column}"));
}
if let Some(clause) = &node.clause {
fields.push(format!("\"clause\":\"{}\"", escape(clause)));
}
fields.push(format!("\"subgoals\":[{}]", children.join(",")));
format!("{{{}}}", fields.join(","))
}
pub fn query_document(query_text: &str, answers: &[Answer]) -> String {
let outcome = if answers.is_empty() {
"none"
} else {
"solutions"
};
let rendered: Vec<String> = answers.iter().map(answer_object).collect();
format!(
"{{\"query\":\"{}\",\"outcome\":\"{outcome}\",\"answers\":[{}]}}",
escape(query_text),
rendered.join(","),
)
}
pub fn query_error_document(query_text: &str, message: &str) -> String {
format!(
"{{\"query\":\"{}\",\"outcome\":\"error\",\"error\":{{\"message\":\"{}\"}}}}",
escape(query_text),
escape(message),
)
}
pub fn error_document(
file: &str,
line: Option<usize>,
column: Option<usize>,
message: &str,
) -> String {
let mut fields = vec![format!("\"file\":\"{}\"", escape(file))];
if let Some(line) = line {
fields.push(format!("\"line\":{line}"));
}
if let Some(column) = column {
fields.push(format!("\"column\":{column}"));
}
fields.push(format!("\"message\":\"{}\"", escape(message)));
format!("{{\"error\":{{{}}}}}", fields.join(","))
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn escaping_covers_quotes_backslashes_and_controls() {
assert_eq!(escape(r#"a"b\c"#), r#"a\"b\\c"#);
assert_eq!(escape("a\nb\tc\r"), "a\\nb\\tc\\r");
assert_eq!(escape("\u{01}"), "\\u0001");
assert_eq!(escape("père = 37/2"), "père = 37/2");
}
#[test]
fn documents_take_their_documented_shapes() {
let truth = Answer {
equations: vec![],
disequations: vec![],
constraints: vec![],
explanation: None,
};
assert_eq!(
query_document("?- ok(s1).", &[truth]),
r#"{"query":"?- ok(s1).","outcome":"solutions","answers":[{"equations":[],"disequations":[],"constraints":[]}]}"#
);
assert_eq!(
query_document("?- ok(s2).", &[]),
r#"{"query":"?- ok(s2).","outcome":"none","answers":[]}"#
);
let bound = Answer {
equations: vec!["X = 3".to_string()],
disequations: vec!["X != Y".to_string()],
constraints: vec!["age(alice) = 30".to_string()],
explanation: None,
};
assert_eq!(
query_document("?- q(X).", &[bound]),
r#"{"query":"?- q(X).","outcome":"solutions","answers":[{"equations":["X = 3"],"disequations":["X != Y"],"constraints":["age(alice) = 30"]}]}"#
);
let explained = Answer {
equations: vec!["C = c17".to_string()],
disequations: vec![],
constraints: vec![],
explanation: Some(vec![ProofNode {
goal: "violation(c17)".to_string(),
by: claimr::Resolution::Rule,
line: Some(2),
column: Some(1),
clause: "violation(C) :- k(C, K), { K > 3 }.".to_string().into(),
subgoals: vec![
ProofNode {
goal: "k(c17, 5)".to_string(),
by: claimr::Resolution::Fact,
line: Some(1),
column: Some(1),
clause: Some("k(c17, 5).".to_string()),
subgoals: vec![],
},
ProofNode {
goal: "{ 5 > 3 }".to_string(),
by: claimr::Resolution::Constraint,
line: Some(2),
column: Some(1),
clause: None,
subgoals: vec![],
},
],
}]),
};
assert_eq!(
query_document("?- violation(C).", &[explained]),
r#"{"query":"?- violation(C).","outcome":"solutions","answers":[{"equations":["C = c17"],"disequations":[],"constraints":[],"explanation":[{"goal":"violation(c17)","by":"rule","line":2,"column":1,"clause":"violation(C) :- k(C, K), { K > 3 }.","subgoals":[{"goal":"k(c17, 5)","by":"fact","line":1,"column":1,"clause":"k(c17, 5).","subgoals":[]},{"goal":"{ 5 > 3 }","by":"constraint","line":2,"column":1,"subgoals":[]}]}]}]}"#
);
assert_eq!(
query_error_document("?- q(X).", "boom"),
r#"{"query":"?- q(X).","outcome":"error","error":{"message":"boom"}}"#
);
assert_eq!(
error_document("f.claimr", Some(2), Some(1), "Expected Dot."),
r#"{"error":{"file":"f.claimr","line":2,"column":1,"message":"Expected Dot."}}"#
);
assert_eq!(
error_document("f.claimr", None, None, "cannot read"),
r#"{"error":{"file":"f.claimr","message":"cannot read"}}"#
);
}
}