Make parenthesis break binding on dtuples #3317
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mtzguido
added a commit
to mtzguido/pulse
that referenced
this pull request
Jun 17, 2024
In preparation for FStarLang/FStar#3317
mtzguido
added a commit
to mtzguido/FStar
that referenced
this pull request
Jun 17, 2024
This patch automatically generated by adding this patch to ToSyntax.fst:
```
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index e0ddf1b9a4..aeb75732db 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -1173,13 +1173,25 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an
| Op(op_star, [lhs;rhs]) when
(Ident.string_of_id op_star = "*" &&
op_as_term env 2 op_star |> Option.isNone) ->
- (* See the comment in parse.mly to understand why this implicitly relies
- * on the presence of a Paren node in the AST. *)
+ (* See the comment in parse.mly to understand why this implicitly relies *)
+ (* on the presence of a Paren node in the AST. *)
+ let print1 (op:ident) : unit =
+ let open FStar.Compiler.Range in
+ let open FStar.Class.Show in
+ let r = range_of_id op in
+ BU.print3 "GGG %s %s %s\n"
+ (file_of_range r |> BU.normalize_file_path)
+ (start_of_range r |> line_of_pos |> show)
+ (start_of_range r |> col_of_pos |> show)
+ in
+ print1 op_star;
+
let rec flatten t = match t.tm with
// * is left-associative
| Op(id, [t1;t2]) when
string_of_id id = "*" &&
op_as_term env 2 op_star |> Option.isNone ->
+ print1 id;
flatten t1 @ [ t2 ]
| _ -> [t]
in
```
And using the following scripts:
fix_all.sh:
```
#/bin/bash
set -eux
IFS=" "
while read marker file line col; do
if [ "x${marker}" != "xGGG" ]; then
continue;
fi
./fix1.sh "${file}" "${line}" "${col}"
done
```
fix1.sh:
```
#/bin/bash
FILE=$1
LINE=$2
COL=$3
sed -i "${LINE}s/^\(.\{${COL}\}\)\*/\1\&/" ${FILE}
```
Then by running `make ci | tee L` we save all positions where `*` was
resolved to tuples, and can run `grep GGG L | ./fix_all.sh` to
automatically fix all of them.
This patch does not cause a snapshot diff, which is a good sign!
A single use of a non-dependent tuple with a refinement on the left
needed a tweak (ValidatedAccess.fst), adding parenthesis as in FStarLang#3317.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As discussed here #2816, sometimes we want to have a refinement on the LHS of a non-dependent tuple, but the parser will still take
(x:a{p x}) & bto be dependent. This PR changes this behavior to make parenthesis break the binding on a tuple type.(Notably function types like
(x:a) -> Tot (b x)do bind across a parenthesis.)Regressions in F* are minor, checking everest now.