53 lines
1.3 KiB
Rust
53 lines
1.3 KiB
Rust
use picolog::ast::Body;
|
|
use picolog::ast::Module;
|
|
|
|
fn main()
|
|
{
|
|
env_logger::builder()
|
|
.filter_level(log::LevelFilter::Debug)
|
|
.format_timestamp(None)
|
|
.init();
|
|
//println!("{:#?}", Module::parse_from_file("1.pl"));
|
|
let module: Module = "
|
|
integer(zero).
|
|
integer(s(X)) :- integer(X).
|
|
|
|
add(X, zero, X).
|
|
add(X, s(Y), Z) :- add(s(X), Y, Z).
|
|
|
|
mult(zero, X, zero).
|
|
mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
|
|
|
|
op(10, yfx, +).
|
|
op(8, yfx, ^).
|
|
op(6, xfy, ::).
|
|
op(2, fx, [).
|
|
op(2, xf, ]).
|
|
op(3, yfx, |).
|
|
|
|
A + B :- test.
|
|
|
|
A ^ B + C :- test.
|
|
A::B::C :- A.
|
|
[Hd|Tl] :- Hd::Tl.
|
|
"
|
|
.into();
|
|
|
|
println!("{}", module);
|
|
let prop: Body = "integer(s(X))".into();
|
|
// let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
|
|
for c in module.prove(&prop)
|
|
{
|
|
println!("true:");
|
|
println!("{}", c.simplified());
|
|
let _ = std::io::stdin().read_line(&mut String::new());
|
|
}
|
|
|
|
// let p: Predicate = "add(s(zero), zero, Y)".into();
|
|
// let p1: Predicate = "add(X, zero, X)".into();
|
|
// // let p: Predicate = "integer(s(zero))".into();
|
|
// // let p1: Predicate = "integer(s(X))".into();
|
|
// println!("{}", p.matches(&p1).unwrap());
|
|
//
|
|
}
|