Skip to content

Commit 30a97f4

Browse files
committed
Superpositions
1 parent fcc857d commit 30a97f4

File tree

7 files changed

+72
-8
lines changed

7 files changed

+72
-8
lines changed

crates/benda/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ use pyo3::prelude::*;
66
use pyo3::types::{PyDict, PyFunction, PyString, PyTuple};
77
use rustpython_parser::{parse, Mode};
88
use types::book::Book;
9+
use types::fan::Fan;
910
use types::tree::{Leaf, Node, Tree};
1011
use types::u24::U24;
1112
mod benda_ffi;
@@ -142,5 +143,6 @@ fn benda(_py: Python, m: &Bound<'_, PyModule>) -> PyResult<()> {
142143
m.add_class::<Tree>()?;
143144
m.add_class::<Node>()?;
144145
m.add_class::<Leaf>()?;
146+
m.add_class::<Fan>()?;
145147
Ok(())
146148
}

crates/benda/src/types/book.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,12 @@ use std::vec;
55
use bend::fun::{self, Book as BendBook, Name, Rule};
66
use bend::imp::{self, Expr, Stmt};
77
use indexmap::IndexMap;
8-
use num_traits::ToPrimitive;
98
use pyo3::exceptions::PyException;
109
use pyo3::prelude::*;
1110
use pyo3::types::{PyString, PyTuple};
1211
use pyo3::PyTypeInfo;
1312

13+
use super::fan::Fan;
1414
use super::user_adt::{from_term_into_adt, UserAdt};
1515
use super::{extract_type_raw, BendType};
1616
use crate::benda_ffi;
@@ -275,6 +275,10 @@ impl Definition {
275275
if let Ok(new_term) = term.extract::<Term>() {
276276
u_type = Some(new_term.term);
277277
}
278+
} else if let Ok(term) = arg.downcast::<Fan>() {
279+
if let Ok(new_term) = term.extract::<Fan>() {
280+
u_type = Some(new_term.term);
281+
}
278282
} else {
279283
let adt = UserAdt::new(arg.clone(), &b);
280284

crates/benda/src/types/fan.rs

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
use bend::fun::Term;
2+
use pyo3::types::{PyString, PyTuple, PyTupleMethods};
3+
use pyo3::{pyclass, pymethods, Bound, Py, PyAny};
4+
5+
use crate::types::extract_type_raw;
6+
7+
#[pyclass(name = "Fan")]
8+
#[derive(Clone, Debug, Default)]
9+
pub struct Fan {
10+
pub term: Term,
11+
}
12+
13+
#[pymethods]
14+
impl Fan {
15+
#[new]
16+
#[pyo3(signature = (*args))]
17+
fn new(args: Bound<'_, PyTuple>) -> Self {
18+
let mut elements: Vec<Term> = vec![];
19+
for arg in args.iter() {
20+
let new_arg =
21+
extract_type_raw(arg.clone()).unwrap().to_bend().unwrap();
22+
let u_type = Some(new_arg.clone().to_fun());
23+
24+
if let Some(u_type) = u_type {
25+
elements.push(u_type);
26+
}
27+
}
28+
29+
let fan = bend::fun::Term::Fan {
30+
fan: bend::fun::FanKind::Tup,
31+
tag: bend::fun::Tag::Static,
32+
els: elements,
33+
};
34+
35+
Self { term: fan }
36+
}
37+
}

crates/benda/src/types/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ use user_adt::UserAdt;
1212

1313
pub mod book;
1414
pub mod f24;
15+
pub mod fan;
1516
pub mod i24;
1617
pub mod tree;
1718
pub mod u24;

docs/FFI.md

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,3 +98,23 @@ sorted_list = book.defs.Sort(my_list).to_adt(book.adts.List)
9898
```
9999

100100
This way you can convert the `Term` object into a ADT to use complex data structures in Python.<br>
101+
102+
## Superpositions
103+
104+
Use [superpositions](https://gist.github.com/VictorTaelin/9061306220929f04e7e6980f23ade615) to boost your code performance. Superpositions are a way to call a Bend function multiple times using a `Tuple` of values.<br>
105+
Example:
106+
```python
107+
import benda
108+
book = benda.load_book_from_file("./examples/sat_solver.bend")
109+
110+
pred = book.defs.pred
111+
112+
x1 = benda.Fan(0,1)
113+
x2 = benda.Fan(0,1)
114+
115+
result = pred(x1,x2)
116+
print("Result: ", result)
117+
118+
```
119+
120+
Here, Fan represents a superposition of values. This code applies the `pred` function to all the possible values of x1 and x2. The result is a superposition of the results of the function applied to all the possible values of x1 and x2.<br>

examples/sat_solver.bend

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,6 @@ pred = (λx1 λx2
22
let nx1=(== x1 0)
33
let nx2=(== x2 0)
44
let res=(&(&(| x1 x2) (| x1 nx2)) (| nx1 x2))
5-
((x1, x2), res))
5+
(res))
6+
7+
main = (pred(0, 1)(0, 1))

examples/sat_solver.py

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,11 @@
55
pred = book.defs.pred
66

77
def main():
8-
x1 = [0,1]
9-
x2 = [0,1]
8+
x1 = benda.Fan(0,1)
9+
x2 = benda.Fan(0,1)
1010

11-
for i in x1:
12-
for x in x2:
13-
result = pred(i, x)
14-
print("Result: ", result)
11+
result = pred(x1,x2)
12+
print("Result: ", result)
1513

1614

1715
if __name__ == "__main__":

0 commit comments

Comments
 (0)