logic_eval/
lib.rs

1#![doc = include_str!("../README.md")]
2
3mod parse;
4mod prove;
5
6// === Re-exports ===
7
8pub use parse::{
9    inner::VAR_PREFIX,
10    inner::{Parse, parse_str},
11    repr::{Clause, ClauseDataset, Expr, Predicate, Term},
12    text::Name,
13};
14pub use prove::{
15    db::{ClauseIter, ClauseRef, Database},
16    prover::ProveCx,
17};
18
19pub mod intern {
20    pub use any_intern::*;
21}
22
23use std::{
24    borrow::Borrow,
25    collections::HashMap,
26    error::Error as StdError,
27    fmt::{self, Debug, Display},
28    hash::{BuildHasherDefault, Hash, Hasher},
29    result::Result as StdResult,
30};
31
32// === Hash map and set used within this crate ===
33
34pub(crate) type Map<K, V> = HashMap<K, V, fxhash::FxBuildHasher>;
35
36#[derive(Default, Clone, Copy)]
37struct PassThroughHasher {
38    hash: u64,
39}
40
41impl Hasher for PassThroughHasher {
42    fn write(&mut self, _bytes: &[u8]) {
43        panic!("u64 is only allowed");
44    }
45
46    fn write_u64(&mut self, i: u64) {
47        self.hash = i;
48    }
49
50    fn finish(&self) -> u64 {
51        self.hash
52    }
53}
54
55pub(crate) type PassThroughState = BuildHasherDefault<PassThroughHasher>;
56
57// === Result/Error used within this crate ===
58
59pub(crate) type Result<T> = StdResult<T, Error>;
60pub(crate) type Error = Box<dyn StdError + Send + Sync>;
61
62// === Interning dependency ===
63
64pub trait Intern {
65    type InternedStr<'a>: AsRef<str> + Borrow<str> + Clone + Eq + Ord + Hash + Debug + Display
66    where
67        Self: 'a;
68
69    fn intern_formatted_str<T: Display + ?Sized>(
70        &self,
71        value: &T,
72        upper_size: usize,
73    ) -> StdResult<Self::InternedStr<'_>, fmt::Error>;
74
75    fn intern_str(&self, text: &str) -> Self::InternedStr<'_> {
76        self.intern_formatted_str(text, text.len()).unwrap()
77    }
78}
79
80impl Intern for any_intern::DroplessInterner {
81    type InternedStr<'a>
82        = any_intern::Interned<'a, str>
83    where
84        Self: 'a;
85
86    fn intern_formatted_str<T: Display + ?Sized>(
87        &self,
88        value: &T,
89        upper_size: usize,
90    ) -> StdResult<Self::InternedStr<'_>, fmt::Error> {
91        self.intern_formatted_str(value, upper_size)
92    }
93
94    fn intern_str(&self, text: &str) -> Self::InternedStr<'_> {
95        self.intern(text)
96    }
97}
98
99impl Intern for any_intern::Interner {
100    type InternedStr<'a>
101        = any_intern::Interned<'a, str>
102    where
103        Self: 'a;
104
105    fn intern_formatted_str<T: Display + ?Sized>(
106        &self,
107        value: &T,
108        upper_size: usize,
109    ) -> StdResult<Self::InternedStr<'_>, fmt::Error> {
110        self.intern_formatted_str(value, upper_size)
111    }
112
113    fn intern_str(&self, text: &str) -> Self::InternedStr<'_> {
114        self.intern_dropless(text)
115    }
116}
117
118// === Type aliases for complex `Intern` related types ===
119
120pub(crate) use intern_alias::*;
121#[allow(unused)]
122mod intern_alias {
123    use super::{Intern, parse, prove};
124    pub(crate) type NameIn<'int, Int> = parse::text::Name<<Int as Intern>::InternedStr<'int>>;
125    pub(crate) type TermIn<'int, Int> = parse::repr::Term<NameIn<'int, Int>>;
126    pub(crate) type ExprIn<'int, Int> = parse::repr::Expr<NameIn<'int, Int>>;
127    pub(crate) type ClauseIn<'int, Int> = parse::repr::Clause<NameIn<'int, Int>>;
128    pub(crate) type UniqueTermArrayIn<'int, Int> = prove::repr::UniqueTermArray<NameIn<'int, Int>>;
129    pub(crate) type TermStorageIn<'int, Int> = prove::repr::TermStorage<NameIn<'int, Int>>;
130    pub(crate) type ClauseDatasetIn<'int, Int> = parse::repr::ClauseDataset<NameIn<'int, Int>>;
131    pub(crate) type Name2Int<'int, Int> =
132        prove::prover::IdxMap<'int, NameIn<'int, Int>, prove::prover::Integer, Int>;
133    pub(crate) type Int2Name<'int, Int> =
134        prove::prover::IdxMap<'int, prove::prover::Integer, NameIn<'int, Int>, Int>;
135}
logic_eval/lib.rs

logic_eval/
lib.rs
