1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

#![recursion_limit = "1024"]
#![cfg_attr(feature = "bench", feature(test))]

pub mod db;
pub mod error;
pub mod interner;
pub mod lowering;
pub mod program;
pub mod program_environment;
pub mod query;
pub mod test_macros;
pub mod tls;

use chalk_engine::solve::SLGSolver;
use chalk_ir::interner::HasInterner;
use chalk_ir::Binders;
use chalk_recursive::{Cache, RecursiveSolver};
use chalk_solve::Solver;
use interner::ChalkIr;

pub use interner::{Identifier, RawId};

#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum TypeSort {
    Adt,
    FnDef,
    Closure,
    Trait,
    Opaque,
    Coroutine,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
pub struct Unit;

impl HasInterner for Unit {
    type Interner = ChalkIr;
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct TypeKind {
    pub sort: TypeSort,
    pub name: Identifier,
    pub binders: Binders<Unit>,
}

#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
pub enum SolverChoice {
    /// Run the SLG solver, producing a Solution.
    SLG {
        max_size: usize,
        expected_answers: Option<usize>,
    },
    /// Run the recursive solver.
    Recursive {
        overflow_depth: usize,
        caching_enabled: bool,
        max_size: usize,
    },
}

impl SolverChoice {
    /// Returns specific SLG parameters.
    pub fn slg(max_size: usize, expected_answers: Option<usize>) -> Self {
        SolverChoice::SLG {
            max_size,
            expected_answers,
        }
    }

    /// Returns the default SLG parameters.
    pub fn slg_default() -> Self {
        SolverChoice::slg(10, None)
    }

    /// Returns the default recursive solver setup.
    pub fn recursive_default() -> Self {
        SolverChoice::Recursive {
            overflow_depth: 100,
            caching_enabled: true,
            max_size: 30,
        }
    }

    /// Returns a recursive solver with specific parameters.
    pub fn recursive(max_size: usize, overflow_depth: usize) -> Self {
        SolverChoice::Recursive {
            overflow_depth,
            caching_enabled: true,
            max_size,
        }
    }

    pub fn into_solver(self) -> Box<dyn Solver<ChalkIr>> {
        match self {
            SolverChoice::SLG {
                max_size,
                expected_answers,
            } => Box::new(SLGSolver::new(max_size, expected_answers)),
            SolverChoice::Recursive {
                overflow_depth,
                caching_enabled,
                max_size,
            } => Box::new(RecursiveSolver::new(
                overflow_depth,
                max_size,
                if caching_enabled {
                    Some(Cache::default())
                } else {
                    None
                },
            )),
        }
    }
}

impl Default for SolverChoice {
    fn default() -> Self {
        SolverChoice::slg(10, None)
    }
}