@@ -4,45 +4,14 @@ This section goes over a few different concepts that are crucial to
4
4
understanding how ` chalk-engine ` works, without going over the exact solving
5
5
logic.
6
6
7
- ## ` Context ` , ` ContextOps ` , and ` InferenceTable `
8
-
9
- ### ` Context `
10
-
11
- The [ ` Context ` ] trait is the primary bridge between Chalk internal logic and
12
- external types. In addition actually * defining* the types (via associated
13
- types), it also contains associated functions to convert or extract
14
- information from those types. Overall, this allows the types to be basically
15
- opaque to the engine internals. Functions in the trait are agnostic to specific
16
- program or environment details, since they lack a ` &self ` argument.
17
-
18
- To give an example, there is an associated [ ` Goal ` ] type. However, Chalk doesn't
19
- know how to solve this. Instead, it has to be converted an ` HhGoal ` via the
20
- ` Context::into_hh_goal ` function. This will be coverted more in the ` Goals `
21
- section.
22
-
23
- ### ` ContextOps `
24
-
25
- The [ ` ContextOps ` ] trait contains functions that may specifically require
26
- information a specific program or environment. For example, the
27
- ` program_clauses ` function gives potential ways to prove a ` Goal ` , but obviously
28
- it requires knowing the program (for example, what types, traits, and impls
29
- there are). Functions in this trait all take a ` &self ` argument.
30
-
31
- ### ` InferenceTable `
32
-
33
- The [ ` InferenceTable ` ] is a super trait to the [ ` UnificationOps ` ] , [ ` TruncateOps ` ] ,
34
- and [ ` ResolventOps ` ] . Each of these contains functions that track the state of
35
- specific parts of the program. Importantly, these operations can dynamically
36
- change the state of the logic itself.
37
-
38
7
## Goals
39
8
40
9
A "goal" in Chalk can be thought of as "something we want to prove". The engine
41
10
itself understands ` HhGoal ` s. ` HHGoal ` s consist of the most basic logic,
42
11
such as introducing Binders (` Forall ` or ` Exists ` ) or combining goals (` All ` ).
43
- On the other hand, ` Context:: Goal` represents an opaque goal generated
12
+ On the other hand, ` Goal ` represents an opaque goal generated
44
13
externally. As such, it may contain any extra information or may be interned.
45
- When solving a logic predicate, Chalk will lazily convert ` Context:: Goal` s
14
+ When solving a logic predicate, Chalk will lazily convert ` Goal ` s
46
15
into ` HHGoal ` s.
47
16
48
17
There are three types of completely opaque ` HhGoal ` s that Chalk can solve:
@@ -77,11 +46,10 @@ goals that depend on this goal.
77
46
78
47
However, oftentimes, this is not what external crates want when solving for a
79
48
goal. Instead, the may want a * unique* solution to this goal. Indeed, when we
80
- solve for a given root [ ` Goal ` ] , we return a since [ ` Solution ` ] . It is up to the
81
- implementation of [ ` Context ` ] to decide how a ` Solution ` is made, given a possibly
82
- infinite set of answers. One of example of this is the
49
+ solve for a given root [ ` Goal ` ] , we return a single [ ` Solution ` ] . The
83
50
[ ` AntiUnifier ` ] ( https://rust-lang.github.io/chalk/chalk_engine/slg/aggregate/struct.AntiUnifier.html )
84
- from ` chalk-solve ` , which finds a minimal generalization of answers which don't
51
+ struct from ` chalk-solve ` then finds that solution, by finding a minimal
52
+ generalization of answers which don't
85
53
unify. (For the example above, it would return only ` Ambiguous ` , since ` A ` and
86
54
` B ` can't unify.)
87
55
@@ -91,7 +59,7 @@ An [`ExClause`] is described in literature as `A :- D | G` or
91
59
` A holds given that G holds with D delayed goals ` . In ` chalk-engine ` , an
92
60
` ExClause ` stores the current state of proving a goal, including existing
93
61
substitutions already found, subgoals yet to be proven, or delayed subgoals. A
94
- [ ` Strand ` ] wraps both an [ ` ExClause ` ] and an [ ` InferenceTable ` ] together.
62
+ [ ` Strand ` ] wraps both an [ ` ExClause ` ] and an [ ` TruncatingInferenceTable ` ] together.
95
63
96
64
## Tables and Forests
97
65
@@ -110,15 +78,15 @@ stack).
110
78
111
79
[ `Context` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
112
80
[ `ContextOps` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html
113
- [ `InferenceTable ` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.InferenceTable .html
114
- [ `Solution` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context .html#associatedtype.Solution
81
+ [ `TruncatingInferenceTable ` ] : https://rust-lang.github.io/chalk/chalk_engine/slg/struct.TruncatingInferenceTable .html
82
+ [ `Solution` ] : https://rust-lang.github.io/chalk/chalk_solve/solve/enum.Solution .html
115
83
[ `ExClause` ] : https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html
116
84
[ `Strand` ] : https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html
117
85
[ `Table` ] : https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html
118
86
[ `Forest` ] : https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html
119
- [ `Goal` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context .html#associatedtype.Goal
87
+ [ `Goal` ] : https://rust-lang.github.io/chalk/chalk_ir/struct.Goal .html
120
88
[ `UnificationOps` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.UnificationOps.html
121
89
[ `TruncateOps` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.TruncateOps.html
122
90
[ `ResolventOps` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.ResolventOps.html
123
- [ `ProgramClause` ] : https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context .html#associatedtype.ProgramClause
91
+ [ `ProgramClause` ] : https://rust-lang.github.io/chalk/chalk_ir/struct.ProgramClause .html
124
92
[ `Answer` ] : https://rust-lang.github.io/chalk/chalk_engine/struct.Answer.html
0 commit comments