From c0ad56a745d11cd7e6552b49311a47aa9bc5ecaf Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 23 Jan 2024 23:31:43 +0100 Subject: [PATCH] move Decode from support/ to src/ for more visibility Suggested-by: Neven Villani --- README.md | 2 +- src/{support => }/Decode.ml | 5 +++++ src/Decode.mli | 21 +++++++++++++++++++++ src/Unif.ml | 2 +- src/support/Decode.mli | 3 --- 5 files changed, 28 insertions(+), 5 deletions(-) rename src/{support => }/Decode.ml (85%) create mode 100644 src/Decode.mli delete mode 100644 src/support/Decode.mli diff --git a/README.md b/README.md index 1ee347c..c20bcc6 100644 --- a/README.md +++ b/README.md @@ -373,7 +373,7 @@ you prefer). - `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 - 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 support code, but you do not need to.) diff --git a/src/support/Decode.ml b/src/Decode.ml similarity index 85% rename from src/support/Decode.ml rename to src/Decode.ml index 498df2c..4ee2fe8 100644 --- a/src/support/Decode.ml +++ b/src/Decode.ml @@ -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 slot = diff --git a/src/Decode.mli b/src/Decode.mli new file mode 100644 index 0000000..a9f1ec3 --- /dev/null +++ b/src/Decode.mli @@ -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 diff --git a/src/Unif.ml b/src/Unif.ml index 5e2e625..f7012c9 100644 --- a/src/Unif.ml +++ b/src/Unif.ml @@ -1,6 +1,6 @@ (* There is nothing that you have to implement in this file/module, 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. *) module UF = UnionFind.Make(UnionFind.StoreMap) diff --git a/src/support/Decode.mli b/src/support/Decode.mli deleted file mode 100644 index 7bbe514..0000000 --- a/src/support/Decode.mli +++ /dev/null @@ -1,3 +0,0 @@ -type env = Unif.Env.t - -val decode : env -> Constraint.variable -> STLC.ty