]>
Witch of Git - mukan/blob - src/main.rs
1 use mukan
::{all
, and
, call_fresh
, delay
, eq
, fresh
, or
, reify
, Goal
, State
, Term
, Var
};
6 let term
= call_fresh(|a
| call_fresh(move |b
| or(and(eq(a
, b
), eq(a
, 1)), eq(b
, 2))));
7 for soln
in term
.solve(State
::new()) {
8 println
!("{:?}", reify(soln
));
12 let term
= fresh
!((p
, a
, b
, c
, d
) => {
20 for soln
in term
.solve(State
::new()) {
21 println
!("{:?}", reify(soln
));
25 let term
= fresh
!((a
, b
) => eq(a
, b
));
26 for soln
in term
.solve(State
::new()) {
27 println
!("{:?}", reify(soln
));
31 fn peano(n
: impl Into
<Term
>) -> impl Goal
+ Clone
{
35 fresh
!((r
) => and(eq(n
.clone(), (1, r
)), delay(move || peano(r
)))),
38 let term
= fresh
!((n
) => peano(n
));
39 for soln
in term
.solve(State
::new()).take(5) {
40 println
!("{:?}", reify(soln
));
43 fn make_nat(n
: u32) -> Term
{
47 (1, make_nat(n
- 1)).into
()
51 fn term_to_nat(mut n
: &Term
) -> Option
<u32> {
55 Term
::Pair(s
, k
) if &**s
== &Term
::Lit(1) => {
59 Term
::Lit(0) => return Some(res
),
65 fn less(n
: impl Into
<Term
>, m
: impl Into
<Term
>) -> impl Goal
+ Clone
{
69 eq((1, n
.clone()), m
.clone()),
71 eq(m
.clone(), (1, x
)),
74 delay(move || less(n
.clone(), x
.clone()))
80 fn sums_to(n
: impl Into
<Term
>, m
: impl Into
<Term
>, s
: impl Into
<Term
>) -> impl Goal
+ Clone
{
85 and(eq(n
.clone(), 0), eq(m
.clone(), s
.clone())),
87 eq(n
.clone(), (1, x
)),
92 less(m
.clone(), s
.clone()),
93 sums_to(x
, (1, m
.clone()), s
.clone()),
100 println
!("Peano addition!");
101 let (vars
, state
) = State
::with_vars(2);
103 let term
= sums_to(vars
[0], vars
[1], make_nat(sum
));
105 for soln
in term
.solve(state
) {
106 let n
= term_to_nat(&soln
.eval_var(vars
[0])).unwrap
();
107 let m
= term_to_nat(&soln
.eval_var(vars
[1])).unwrap
();
108 print
!("{} + {} = ", n
, m
);
109 std
::io
::stdout().fl
ush
().unwrap
();
113 println
!("Infinite data!");
114 let term
= fresh
!((x
, y
, z
) => all
! {
117 eq(x
, (1, (y
, (1, x
)))),
120 for soln
in term
.solve(State
::new()) {
121 println
!("= {}", soln
);
124 fn unproductive(x
: impl Into
<Term
>) -> impl Goal
+ Clone
{
126 delay(move || unproductive(x
.clone()))
129 println
!("Or Unproductive");
130 let (vars
, state
) = State
::with_vars(2);
131 let goal
= or(peano(vars
[0]), unproductive(vars
[0]));
132 for soln
in goal
.solve(state
).take(5) {
133 println
!("peano {}", term_to_nat(&soln
.eval_var(vars
[0])).unwrap
());
136 fn infinite(x
: Var
) -> impl Goal
+ Clone
{
137 or(eq(x
, x
), delay(move || infinite(x
)))
140 println
!("And Fairness");
141 let goal
= fresh
!((x
) => all
! {
145 for soln
in goal
.solve(State
::new()).take(5) {
146 println
!("{}", soln
);