Skip to content

Commit 41b378c

Browse files
committed
SortDiagram construction on SortTable.
1 parent 2f7f77b commit 41b378c

File tree

19 files changed

+727
-175
lines changed

19 files changed

+727
-175
lines changed

Cargo.toml

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ members = [
33
"mod2",
44
"mod2-lib",
55
"mod2-abs",
6-
"mod2-wl"
6+
# "mod2-wl"
77
]
88
resolver = "3"
99

@@ -18,17 +18,18 @@ readme = "README.md"
1818
publish = false
1919

2020
[workspace.dependencies]
21-
string_cache = "0.8" # String interning
21+
#total_float_wrap = "^0.1.1" # Totally ordered, hashable floating point types.
2222
#ustr = "1.0.0" # String interning
2323
bit-set = "0.8" # NatSet implementation
2424
enumflags2 = "0.7" # BitFlags from an enum
25+
lalrpop-util = { version = "0.22", features = ["lexer", "unicode"] }
26+
num-bigint = "0.4"
27+
num-traits = "0.2"
2528
once_cell = "^1.20" # Lazy statics
26-
rand = "^0.9" # Testing
2729
paste = "^1.0" # Concat identifiers in `implement_data_atom!` macro
30+
rand = "^0.9" # Testing
2831
smallvec = { version = "1.14.0", features = ["union"] }
29-
30-
total_float_wrap = "^0.1.1" # Totally ordered, hashable floating point types.
31-
lalrpop-util = { version = "0.22", features = ["lexer", "unicode"] }
32+
string_cache = "0.8" # String interning
3233

3334
## Logging ##
3435
tracing = "0.1"

README.md

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,44 @@
11
# `mod2-lib`: A pattern matching and term rewriting library
22

3-
- The `mod2-lib` library builds on lessons learned in previous experiments to bring advanced pattern matching algorithms
3+
- The [`mod2-lib`](mod2-lib/README.md) library builds on lessons learned in previous experiments to bring advanced pattern matching algorithms
44
to Rust.
55

6-
- The `mod2` crate is a small Maude-like language meant to exercise the algorithms in `mod2-lib` and stand as a thorough
6+
- The [`mod2`](mod2/README.md) crate is a small Maude-like language meant to exercise the algorithms in `mod2-lib` and stand as a thorough
77
example of how to use `mod2-lib`.
88

9-
- The `mod2-abs` crate is an abstraction layer over backend implementations of various generally useful utilities used
9+
- The [`mod2-abs`](mod2-abs/README.md) crate is an abstraction layer over backend implementations of various generally useful utilities used
1010
throughout.
1111

1212
This project is a work in progress. For a more complete work, check out [Loris](https://github.com/rljacobson/loris).
1313

1414
# Status
1515

16+
## Syntax for mod2
17+
1618
- [X] Lexer & parser
1719
- [X] M-expression
1820
- [X] symbol declarations
1921
- [X] modules syntax
2022
- [ ] Module & submodule semantics
2123
- [ ] custom operators
2224
- [ ] Imperative Language
23-
- [ ] match
24-
- [ ] match_all
25-
- [ ] unify
26-
- [ ] replace
27-
- [ ] replace_all
25+
26+
## mod2-lib algorithms
27+
28+
- [ ] Sort infrastructure
29+
- [ ] Dagify
30+
- [ ] Compilers
31+
- [ ] automata
32+
- [ ] Stack Machine
33+
- [ ] Match
34+
- [ ] Free theory
35+
- [ ] Free net
36+
- [ ] Built-ins
37+
- [ ] Variable theory
38+
- [ ] Other theories
39+
- [ ] CUI
40+
- [ ] AU
41+
- [ ] ACU
2842

2943
# License and Authorship
3044

mod2-abs/Cargo.toml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,11 @@ publish.workspace = true
1010
readme = "README.md"
1111

1212
[dependencies]
13-
string_cache.workspace = true
1413
bit-set.workspace = true
14+
num-bigint.workspace = true
15+
num-traits.workspace = true
1516
smallvec.workspace = true
17+
string_cache.workspace = true
1618

1719
tracing.workspace = true
1820
tracing-subscriber.workspace = true

mod2-abs/src/hash.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ mod tests {
181181
assert_eq!(hasher.finish(), hash_result);
182182
}
183183

184-
184+
/*
185185
#[test]
186186
fn test_fast_hasher_api() {
187187
let mut hasher = FastHasher::new();
@@ -198,11 +198,13 @@ mod tests {
198198
.wrapping_add(3u64)
199199
.shl(7u64)
200200
.wrapping_add(4u64);
201+
// Seems like the following should be `hash2(0, v1*v2)`.
201202
assert_eq!(hasher.finish(), hash2(v1, v2));
202203
203204
1u32.hash(&mut hasher);
204205
assert_eq!(hasher.finish(), hash2(hash2(v1, v2), 1u64));
205206
}
207+
*/
206208

207209
#[test]
208210
fn test_build_hasher() {

mod2-abs/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,9 @@ mod erased;
4040
mod graph;
4141
mod unsafe_ptr;
4242

43+
// Arbitrary precision arithmetic
44+
pub mod numeric;
45+
4346
// region Hashing data structures
4447
use std::collections::HashSet as StdHashSet;
4548
use std::collections::HashMap as StdHashMap;

mod2-abs/src/nat_set.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,11 @@ impl NatSet {
2323
self.0.iter().next()
2424
}
2525

26+
#[inline(always)]
27+
pub fn max_value(&self) -> Option<usize> {
28+
self.0.iter().last()
29+
}
30+
2631
#[inline(always)]
2732
pub fn contains(&self, value: usize) -> bool {
2833
self.0.contains(value)

mod2-abs/src/numeric.rs

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
/*!
2+
3+
Arbitrary precision arithmetic and number traits.
4+
5+
*/
6+
7+
8+
9+
// Arbitrary precision arithmetic
10+
pub use num_bigint::{
11+
BigInt,
12+
BigUint,
13+
ParseBigIntError,
14+
ToBigInt,
15+
ToBigUint,
16+
Sign
17+
};
18+
19+
pub use num_traits as traits;

mod2-lib/Cargo.toml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@ keywords = ["pattern-matching", "matching-algorithms", "unification", "term-r
1212
categories = ["algorithms", "compilers", "mathematics", "science", "parsing"]
1313

1414
[features]
15-
default = ["gc_debug"]
15+
default = ["gc_debug", "debug"]
1616

17+
debug = []
1718
gc_debug = []
1819
multithreaded = []
1920

mod2-lib/src/api/built_in/mod.rs

Lines changed: 74 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ use crate::{
2525
SortPtr
2626
},
2727
symbol::{
28+
OpDeclaration,
2829
SymbolAttribute,
2930
SymbolCore,
3031
SymbolType
@@ -34,7 +35,6 @@ use crate::{
3435

3536
pub use nonalgebraic_term::*;
3637
pub use nonalgebraic_symbol::*;
37-
use crate::core::symbol::OpDeclaration;
3838

3939
// Built-in Types
4040
pub type Bool = bool;
@@ -48,72 +48,74 @@ pub type NaturalNumber = u64;
4848
pub type StringBuiltIn = String;
4949

5050

51-
static BUILT_IN_SORTS: Lazy<Arc<HashMap<IString, Sort>>> = Lazy::new(|| {
52-
let mut sorts = HashMap::new();
51+
macro_rules! make_symbol {
52+
($sort_name:expr, $symbol_name:expr, $symbol_type:expr) => {
53+
{
54+
let sort = get_built_in_sort($sort_name).unwrap();
55+
let symbol_name = IString::from($symbol_name);
56+
let symbol_core = SymbolCore::new(
57+
symbol_name.clone(),
58+
Arity::Value(0),
59+
SymbolAttribute::Constructor.into(),
60+
$symbol_type,
61+
);
62+
let symbol = Box::new(BoolSymbol::new(symbol_core));
63+
let mut symbol_ptr = SymbolPtr::new(Box::into_raw(symbol));
64+
let op_declaration = OpDeclaration::new(smallvec![sort], true.into());
65+
let symbol_ptr_copy = symbol_ptr; // Force copy
66+
symbol_ptr.add_op_declaration(symbol_ptr_copy, op_declaration);
67+
68+
($symbol_name, symbol_ptr)
69+
}
70+
};
71+
}
72+
73+
static BUILT_IN_SORTS: Lazy<HashMap<&'static str, Sort>> = Lazy::new(|| {
74+
let mut sorts = HashMap::default();
5375
// ToDo: Warn when a user shadows a built-in.
5476
{
55-
let name = IString::from("Float");
56-
let sort = Sort::new(name.clone());
77+
let name = "Float";
78+
let sort = Sort::new(IString::from(name));
5779
sorts.insert(name, sort);
5880
}
5981
{
60-
let name = IString::from("Integer");
61-
let sort = Sort::new(name.clone());
82+
let name = "Integer";
83+
let sort = Sort::new(IString::from(name));
6284
sorts.insert(name, sort);
6385
}
6486
{
65-
let name = IString::from("NaturalNumber");
66-
let sort = Sort::new(name.clone());
87+
let name = "NaturalNumber";
88+
let sort = Sort::new(IString::from(name));
6789
sorts.insert(name, sort);
6890
}
6991
{
70-
let name = IString::from("String");
71-
let sort = Sort::new(name.clone());
92+
let name = "String";
93+
let sort = Sort::new(IString::from(name));
7294
sorts.insert(name, sort);
7395
}
7496
{
75-
let name = IString::from("Bool");
76-
let sort = Sort::new(name.clone());
97+
let name = "Bool";
98+
let sort = Sort::new(IString::from(name));
7799
sorts.insert(name, sort);
78100
}
79101
{
80-
let name = IString::from("Any");
81-
let sort = Sort::new(name.clone());
102+
let name = "Any";
103+
let sort = Sort::new(IString::from(name));
82104
sorts.insert(name, sort);
83105
}
84106
{
85-
let name = IString::from("None");
86-
let sort = Sort::new(name.clone());
107+
let name = "None";
108+
let sort = Sort::new(IString::from(name));
87109
sorts.insert(name, sort);
88110
}
89-
Arc::new(sorts)
111+
112+
println!("Initialized built-in sorts: {:?}", sorts);
113+
114+
sorts
90115
});
91116

92-
macro_rules! make_symbol {
93-
($sort_name:expr, $symbol_name:expr, $symbol_type:expr) => {
94-
{
95-
let sort_name = IString::from($sort_name);
96-
let sort = get_built_in_sort(&sort_name).unwrap();
97-
let symbol_name = IString::from($symbol_name);
98-
let mut symbol_core = SymbolCore::new(
99-
symbol_name.clone(),
100-
Arity::Value(0),
101-
SymbolAttribute::Constructor.into(),
102-
$symbol_type,
103-
// sort,
104-
);
105-
let op_declaration = OpDeclaration::new(smallvec![sort], true.into());
106-
symbol_core.add_op_declaration(op_declaration);
107-
108-
let symbol = Box::new(BoolSymbol::new(symbol_core));
109-
let symbol_ptr = SymbolPtr::new(Box::into_raw(symbol));
110-
(symbol_name, symbol_ptr)
111-
}
112-
};
113-
}
114-
115-
static BUILT_IN_SYMBOLS: Lazy<Arc<HashMap<IString, SymbolPtr>>> = Lazy::new(|| {
116-
let mut symbols = HashMap::new();
117+
static BUILT_IN_SYMBOLS: Lazy<HashMap<&'static str, SymbolPtr>> = Lazy::new(|| {
118+
let mut symbols = HashMap::default();
117119
// ToDo: Warn when a user shadows a built-in.
118120
// Bool true
119121
{
@@ -145,19 +147,41 @@ static BUILT_IN_SYMBOLS: Lazy<Arc<HashMap<IString, SymbolPtr>>> = Lazy::new(|| {
145147
let (symbol_name, symbol_ptr) = make_symbol!("NaturalNumber", "NaturalNumber", SymbolType::NaturalNumber);
146148
symbols.insert(symbol_name, symbol_ptr);
147149
}
148-
149-
Arc::new(symbols)
150+
151+
symbols
150152
});
151153

152154
pub fn get_built_in_sort(name: &str) -> Option<SortPtr> {
153-
let name = IString::from(name);
154-
let sort: &Sort = BUILT_IN_SORTS.get(&name)?;
155-
155+
let sort: &Sort = BUILT_IN_SORTS.get(name)?;
156156
Some(SortPtr::new((sort as *const Sort) as *mut Sort))
157157
}
158158

159159
pub fn get_built_in_symbol(name: &str) -> Option<SymbolPtr> {
160-
let name = IString::from(name);
161-
let symbol: SymbolPtr = *BUILT_IN_SYMBOLS.get(&name)?;
160+
let symbol: SymbolPtr = *BUILT_IN_SYMBOLS.get(name)?;
162161
Some(symbol)
163162
}
163+
164+
165+
#[cfg(test)]
166+
mod tests {
167+
use std::ops::Deref;
168+
use super::*;
169+
170+
#[test]
171+
fn test_built_in_sorts() {
172+
let maybe_bool_sort = get_built_in_sort("Bool");
173+
assert!(maybe_bool_sort.is_some());
174+
175+
let bool_sort = maybe_bool_sort.unwrap();
176+
assert_eq!(bool_sort.name.deref(), "Bool")
177+
}
178+
179+
#[test]
180+
fn test_built_in_symbols() {
181+
let maybe_true_symbol = get_built_in_symbol("true");
182+
assert!(maybe_true_symbol.is_some());
183+
184+
let true_symbol = maybe_true_symbol.unwrap();
185+
assert_eq!(true_symbol.name().deref(), "true")
186+
}
187+
}

0 commit comments

Comments
 (0)