1#![doc = include_str!("../README.md")]
2
3mod parse;
4mod prove;
5
6pub use parse::{
9 common::{Intern, InternedStr, StrInterner},
10 inner::VAR_PREFIX,
11 inner::{parse_str, Parse},
12 repr::{Clause, ClauseDataset, Expr, Predicate, Term},
13 text::Name,
14};
15pub use prove::{
16 common::Atom,
17 db::{ClauseIter, ClauseRef, Database},
18 prover::ProveCx,
19};
20
21pub mod intern {
22 pub use any_intern::*;
23}
24
25pub(crate) use intern_alias::*;
28#[allow(unused)]
29mod intern_alias {
30 use crate::{parse, prove, Intern};
31 pub(crate) type NameIn<'int, Int> = parse::text::Name<<Int as Intern>::Interned<'int>>;
32 pub(crate) type TermIn<'int, Int> = parse::repr::Term<NameIn<'int, Int>>;
33 pub(crate) type ExprIn<'int, Int> = parse::repr::Expr<NameIn<'int, Int>>;
34 pub(crate) type ClauseIn<'int, Int> = parse::repr::Clause<NameIn<'int, Int>>;
35 pub(crate) type UniqueTermArrayIn<'int, Int> = prove::repr::UniqueTermArray<NameIn<'int, Int>>;
36 pub(crate) type TermStorageIn<'int, Int> = prove::repr::TermStorage<NameIn<'int, Int>>;
37 pub(crate) type ClauseDatasetIn<'int, Int> = parse::repr::ClauseDataset<NameIn<'int, Int>>;
38}
39
40pub(crate) type Map<K, V> = fxhash::FxHashMap<K, V>;
41pub(crate) type IndexMap<K, V> = indexmap::IndexMap<K, V, fxhash::FxBuildHasher>;
42pub(crate) type IndexSet<T> = indexmap::IndexSet<T, fxhash::FxBuildHasher>;
43pub(crate) type PassThroughIndexMap<K, V> = indexmap::IndexMap<K, V, PassThroughState>;
44
45use std::{
46 error::Error as StdError,
47 hash::{BuildHasherDefault, Hasher},
48 result::Result as StdResult,
49};
50
51#[derive(Default, Clone, Copy)]
52struct PassThroughHasher {
53 hash: u64,
54}
55
56impl Hasher for PassThroughHasher {
57 fn write(&mut self, _bytes: &[u8]) {
58 panic!("u64 is only allowed");
59 }
60
61 fn write_u64(&mut self, i: u64) {
62 self.hash = i;
63 }
64
65 fn finish(&self) -> u64 {
66 self.hash
67 }
68}
69
70pub(crate) type PassThroughState = BuildHasherDefault<PassThroughHasher>;
71
72pub(crate) type Result<T> = StdResult<T, Error>;
75pub(crate) type Error = Box<dyn StdError + Send + Sync>;