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 #3317.
This patch automatically generated by adding this patch to ToSyntax.fst:
And using the following scripts:
fix_all.sh:
fix1.sh:
Then by running
make ci | tee L
we save all positions where*
was resolved to tuples, and can rungrep 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 #3317.