move Decode from support/ to src/ for more visibility

Suggested-by: Neven Villani <neven.villani@crans.org>
This commit is contained in:
Gabriel Scherer 2024-01-23 23:31:43 +01:00
parent e76e32347f
commit c0ad56a745
5 changed files with 28 additions and 5 deletions

View File

@ -373,7 +373,7 @@ you prefer).
- `src/`: the bulk of the code, that place where we expect you to - `src/`: the bulk of the code, that place where we expect you to
work. `src/*.{ml,mli}` are the more important modules that you will work. `src/*.{ml,mli}` are the more important modules that you will
have to modify or use directory. `src/support/*.{ml,mli}` has the have to modify or use directly. `src/support/*.{ml,mli}` has the
less interesting support code. (Again, feel free to modify the less interesting support code. (Again, feel free to modify the
support code, but you do not need to.) support code, but you do not need to.)

View File

@ -1,3 +1,8 @@
(* There is nothing that you have to implement in this file/module,
and no particular need to read its implementation. [Decode.mli]
explains its purpose. *)
type env = Unif.Env.t type env = Unif.Env.t
type slot = type slot =

21
src/Decode.mli Normal file
View File

@ -0,0 +1,21 @@
type env = Unif.Env.t
(** Suppose the unification environment [env] contains the following equations:
?w = ?w1 -> ?w2
?w1 = int
?w2 = bool
?w3 = ?w1 -> ?w4
?w4 : no structure
Then [decode env ?w] will return the type [int -> bool].
Notice on the other hand that [?w3] is of the form [?w1 -> ?w4]
for a still-undertermined variable [?w4]. Any type of the form
[int -> foo] might work, for any [foo], but further progress in
the inference process could end up in a solution incompatible with
any specific choice of [foo]. We decide to decode this into
a fresh (rigid) type variable (which is assumed distinct from
everything else, but nothing else): [?w3] decodes into [int -> α].
*)
val decode : env -> Constraint.variable -> STLC.ty

View File

@ -1,6 +1,6 @@
(* There is nothing that you have to implement in this file/module, (* There is nothing that you have to implement in this file/module,
and no particular need to read its implementation. On the other hand, and no particular need to read its implementation. On the other hand,
you want to understand the interface exposed in [Unif.mli] has it you want to understand the interface exposed in [Unif.mli], as it
is important to implement a constraint solver in Solver.ml. *) is important to implement a constraint solver in Solver.ml. *)
module UF = UnionFind.Make(UnionFind.StoreMap) module UF = UnionFind.Make(UnionFind.StoreMap)

View File

@ -1,3 +0,0 @@
type env = Unif.Env.t
val decode : env -> Constraint.variable -> STLC.ty