Skip to content

Commit

Permalink
normalizer: preserve Meta_desugared (when not beta reducing)
Browse files Browse the repository at this point in the history
Otherwise, the tcnorm call during typechecking will blow away
all the sequence information, causing bad printing.

Fixes #2949
  • Loading branch information
mtzguido committed Nov 30, 2023
1 parent 7e11e10 commit cf987bf
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions src/typechecker/FStar.TypeChecker.Normalize.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1732,6 +1732,10 @@ let rec norm : cfg -> env -> stack -> term -> term =
norm cfg env (Meta(env, Meta_pattern(names, args), t.pos)::stack) head
//meta doesn't block reduction, but we need to put the label back

(* Try to retain Sequence nodes when not normalizing letbindings. *)
| Meta_desugared Sequence when cfg.steps.do_not_unfold_pure_lets ->
norm cfg env (Meta(env,m,t.pos)::stack) head

| Meta_desugared (Machine_integer (_,_)) ->
(* meta doesn't block reduction,
but we need to put the label back *)
Expand Down

0 comments on commit cf987bf

Please sign in to comment.