use std::time::SystemTime;
use std::path::PathBuf;
use avalog::*;
fn main() {
println!("=== Avalog 0.7 ===");
println!("Type `help` for more information.");
let ref parent = match std::env::current_dir() {
Ok(x) => x,
Err(_) => {
eprintln!("Could not get working directory");
return;
}
};
let mut facts = vec![];
let mut settings = ProveSettings {
hide_facts: false,
hide_rules: false,
max_size: Some(600),
reduce: true,
last_import: None,
graph_file: None,
graph_layout: None,
};
loop {
use std::io::{self, Write};
print!("> ");
let mut input = String::new();
io::stdout().flush().unwrap();
match io::stdin().read_line(&mut input) {
Ok(_) => {}
Err(_) => {
println!("ERROR: Could not read input");
continue;
}
};
match input.trim() {
"bye" => break,
"clear" => {facts.clear(); continue}
"hide facts" => {
settings.hide_facts = true;
continue
}
"hide rules" => {
settings.hide_rules = true;
continue
}
"hide all" => {
settings.hide_facts = true;
settings.hide_rules = true;
continue
}
"show facts" => {
settings.hide_facts = false;
continue
}
"show rules" => {
settings.hide_rules = false;
continue
}
"show all" => {
settings.hide_facts = false;
settings.hide_rules = false;
continue
}
"no maxsize" => {
settings.max_size = None;
continue
}
"reload" => {
if let Some(v) = settings.last_import.as_ref() {
input = v.into();
} else {
println!("ERROR: No last import");
continue;
}
}
"graph" => {
export_graph(&facts, &settings, parent);
continue;
}
"no graphf" => {
settings.graph_file = None;
continue;
}
"help" => {print_help(); continue}
"help hide" => {print_help_hide(); continue}
"help pairs" => {print_help_pairs(); continue}
"help roles" => {print_help_roles(); continue}
"help avatars" => {print_help_avatars(); continue}
"help rules" => {print_help_rules(); continue}
"help application" => {print_help_application(); continue}
"help eval" => {print_help_eval(); continue}
"help equality" => {print_help_equality(); continue}
"help inequality" => {print_help_inequality(); continue}
"help list" => {print_help_list(); continue}
"help graph" => {print_help_graph(); continue}
x => {
if x.starts_with("?") {
match parse_str(x[1..].trim(), &parent) {
Ok(pat) => {
search_pat(&pat, &facts, &settings);
continue;
}
Err(err) => {
println!("ERROR:\n{}", err);
continue;
}
}
} else if x.starts_with("prove ") {
match parse_str(x[6..].trim(), &parent) {
Ok(goals) => {
settings.reduce = true;
prove(&goals, &facts, &settings);
continue;
}
Err(err) => {
println!("ERROR:\n{}", err);
continue;
}
}
} else if x.starts_with("provenr ") {
match parse_str(x[8..].trim(), &parent) {
Ok(goals) => {
settings.reduce = false;
prove(&goals, &facts, &settings);
continue;
}
Err(err) => {
println!("ERROR:\n{}", err);
continue;
}
}
} else if x.starts_with("echo ") {
let res: ParseResult = parse_str(x[5..].trim(), parent);
match res {
Ok(facts) => {
println!("{:#?}", facts);
continue;
}
Err(err) => {
println!("ERROR:\n{}", err);
continue;
}
}
} else if x.starts_with("maxsize ") {
match x[8..].trim().parse::<usize>() {
Ok(n) => settings.max_size = Some(n),
Err(_) => eprintln!("ERROR: Could not parse number"),
};
continue;
} else if x.starts_with("import ") {
settings.last_import = Some(input.clone());
} else if x.starts_with("graphf ") {
if let Some(txt) = json_str(x[7..].trim()) {
settings.graph_file = Some(parent.join(&txt));
}
continue;
} else if x.starts_with("graphl ") {
if let Some(txt) = json_str(x[7..].trim()) {
settings.graph_layout = Some(txt);
}
continue;
}
}
}
match parse_str(&input, parent) {
Ok(new_facts) => {
facts.extend(new_facts);
facts.sort();
facts.dedup();
}
Err(err) => {
println!("ERROR:\n{}", err);
continue;
}
};
}
}
fn json_str(txt: &str) -> Option<String> {
use read_token::ReadToken;
let r = ReadToken::new(txt, 0);
if let Some(range) = r.string() {
if let Ok(txt) = r.parse_string(range.length) {
Some(txt)
} else {
println!("ERROR:\nCould not parse string");
None
}
} else {
println!("ERROR:\nExpected string");
None
}
}
pub struct ProveSettings {
pub hide_facts: bool,
pub hide_rules: bool,
pub max_size: Option<usize>,
pub reduce: bool,
pub last_import: Option<String>,
pub graph_file: Option<PathBuf>,
pub graph_layout: Option<String>,
}
fn conclusion(
status: Result<(), Error>,
start_time: SystemTime,
end_time: SystemTime,
settings: &ProveSettings,
) {
println!("");
if status.is_ok() {
println!("OK");
} else {
println!("ERROR");
if let Some(m) = settings.max_size {
if let Err(Error::MaxSize) = status {
println!("Maximum limit reached.");
println!("Use `maxsize <number>` or `no maxsize` to set limit.");
println!("Current maximum number of facts and rules: {}", m);
}
}
}
match end_time.duration_since(start_time) {
Ok(d) => println!("Proof search took {} milliseconds", d.as_millis()),
Err(_) => {}
}
}
fn export_graph(facts: &[Expr], settings: &ProveSettings, parent: &PathBuf) {
use std::fmt::Write;
use std::collections::{HashMap, HashSet};
use std::fs::File;
let start_time = SystemTime::now();
let (res, status) = search_with_accelerator(
&facts,
|e| if let Expr::Rel(_, _) = e {Some(e.clone())}
else if let Expr::RoleOf(_, _) = e {Some(e.clone())}
else {None},
settings.max_size,
&[],
&[],
infer,
&mut Accelerator::new()
);
let end_time = SystemTime::now();
let n: usize = res.len();
let mut nodes: HashSet<Expr> = HashSet::new();
let mut roles: HashMap<Expr, Expr> = HashMap::new();
for e in &res {
if let Expr::Rel(a, b) = e {
if !nodes.contains(a) {nodes.insert((**a).clone());}
if !nodes.contains(b) {nodes.insert((**b).clone());}
} else if let Expr::RoleOf(a, b) = e {
if !roles.contains_key(a) {
roles.insert((**a).clone(), (**b).clone());
}
}
}
conclusion(status, start_time, end_time, settings);
println!("{} results found", n);
let file = if let Some(file) = &settings.graph_file {
parent.join(file)
} else if let Some(last_import) = &settings.last_import {
if let Some(txt) = json_str(last_import[7..].trim()) {
parent.join(txt + ".dot")
} else {
return
}
} else {
parent.join("tmp.dot")
};
println!("Exporting to `{}`", file.clone().into_os_string().into_string().unwrap());
let layout: &str = settings.graph_layout.as_ref().map(|s| &**s).unwrap_or("dot");
let node_color = "#ffffffa0";
let edge_color = "black";
let mut s = String::new();
writeln!(&mut s, "digraph G {{").unwrap();
writeln!(&mut s, " layout={}; edge[penwidth=1,color=\"{}\"]", layout, edge_color).unwrap();
writeln!(&mut s, " node[regular=false,style=filled,fillcolor=\"{}\"]", node_color).unwrap();
for e in &res {
if let Expr::Rel(a, b) = e {
if roles.contains_key(b) {
writeln!(&mut s, " \"{}\" -> \"{}\"[label=\"{}\"];", a, b,
roles.get(b).unwrap()).unwrap();
} else {
writeln!(&mut s, " \"{}\" -> \"{}\";", a, b).unwrap();
}
}
}
writeln!(&mut s, "}}").unwrap();
match File::create(file) {
Ok(mut f) => {
use std::io::Write;
if write!(&mut f, "{}", s).is_err() {
println!("ERROR:\nWhen exporting graph to file");
}
}
Err(_) => {
println!("ERROR:\nCould not create file");
return;
}
};
}
fn search_pat(pat: &[Expr], facts: &[Expr], settings: &ProveSettings) {
if pat.len() == 0 {return};
let pat = &pat[0];
let start_time = SystemTime::now();
let (res, status) = search_with_accelerator(
&facts,
|e| {
let mut vs = vec![];
let mut tail = vec![];
if bind(pat, e, &mut vs, &mut tail) {
Some(e.clone())
} else {
None
}
},
settings.max_size,
&[],
&[],
infer,
&mut Accelerator::new()
);
let end_time = SystemTime::now();
let n: usize = res.len();
for r in res {
println!("{}", r);
}
conclusion(status, start_time, end_time, settings);
println!("{} results found", n);
}
fn prove(goals: &[Expr], facts: &[Expr], settings: &ProveSettings) {
let start_time = SystemTime::now();
let (res, status) = if settings.reduce {
solve_and_reduce_with_accelerator(
&facts,
&goals,
settings.max_size,
&[],
&[],
infer,
Accelerator::constructor(),
)
} else {
solve_with_accelerator(
&facts,
&goals,
settings.max_size,
&[],
&[],
infer,
&mut Accelerator::new(),
)
};
let end_time = SystemTime::now();
let mut count_hidden_facts = 0;
let mut count_hidden_rules = 0;
let mut in_start = true;
for r in &res {
if in_start {
let mut found = false;
for q in facts {
if q == r {
found = true;
break;
}
}
if !found {
in_start = false;
if count_hidden_facts > 0 {
println!("<---oo-o--< {} hidden facts >--o-oo--->", count_hidden_facts);
}
if count_hidden_rules > 0 {
println!("<---oo-o--< {} hidden rules >--o-oo--->", count_hidden_rules);
}
print!("----------------------------------------");
println!("----------------------------------------");
}
}
let rule = if let Expr::Rule(_, _) = r {true} else {false};
let hide = in_start && (!rule && settings.hide_facts ||
rule && settings.hide_rules);
if !hide {
println!("{}", r);
} else {
if !rule {count_hidden_facts += 1};
if rule {count_hidden_rules += 1};
}
}
conclusion(status, start_time, end_time, settings);
}
fn print_help() {print!("{}", include_str!("../assets/help.txt"))}
fn print_help_hide() {print!("{}", include_str!("../assets/help-hide.txt"))}
fn print_help_pairs() {print!("{}", include_str!("../assets/help-pairs.txt"))}
fn print_help_roles() {print!("{}", include_str!("../assets/help-roles.txt"))}
fn print_help_avatars() {print!("{}", include_str!("../assets/help-avatars.txt"))}
fn print_help_rules() {print!("{}", include_str!("../assets/help-rules.txt"))}
fn print_help_application() {print!("{}", include_str!("../assets/help-application.txt"))}
fn print_help_eval() {print!("{}", include_str!("../assets/help-eval.txt"))}
fn print_help_equality() {print!("{}", include_str!("../assets/help-equality.txt"))}
fn print_help_inequality() {print!("{}", include_str!("../assets/help-inequality.txt"))}
fn print_help_list() {print!("{}", include_str!("../assets/help-list.txt"))}
fn print_help_graph() {println!("{}", include_str!("../assets/help-graph.txt"))}