Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Excluding some fixpoint reductions in typechecker #2881

Merged
merged 2 commits into from
Apr 12, 2023
Merged

Excluding some fixpoint reductions in typechecker #2881

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ca050b0
excluding some zetas in the typechecker
mtzguido Apr 6, 2023
3a91840
snap
mtzguido Apr 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 9 additions & 3 deletions ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 2 additions & 1 deletion ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 3 additions & 3 deletions src/typechecker/FStar.TypeChecker.Rel.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1836,7 +1836,7 @@ let simplify_guard env g = match g.guard_f with
| NonTrivial f ->
if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplifying guard %s\n" (Print.term_to_string f);
let f = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.6"
[Env.Beta; Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.NoFullNorm] env f in
[Env.Beta; Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.NoFullNorm; Env.Exclude Env.Zeta] env f in
if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplified guard to %s\n" (Print.term_to_string f);
let f =
let g = U.unmeta f in
Expand Down Expand Up @@ -4944,7 +4944,7 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g
(BU.format1 "Before normalization VC=\n%s\n" (Print.term_to_string vc));
let vc =
Profiling.profile
(fun () -> N.normalize [Env.Eager_unfolding; Env.Simplify; Env.Primops] env vc)
(fun () -> N.normalize [Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.Exclude Env.Zeta] env vc)
(Some (Ident.string_of_lid (Env.current_module env)))
"FStar.TypeChecker.Rel.vc_normalization"
in
Expand Down Expand Up @@ -4974,7 +4974,7 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g
if Options.profile_enabled None "FStar.TypeChecker"
then BU.print1 "Tactic preprocessing produced %s goals\n" (BU.string_of_int (List.length vcs));
let vcs = List.map (fun (env, goal, opts) ->
env, norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.7" [Env.Simplify; Env.Primops] env goal, opts) vcs in
env, norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.7" [Env.Simplify; Env.Primops; Env.Exclude Env.Zeta] env goal, opts) vcs in
let vcs = List.map (fun (env, goal, opts) ->
env.solver.handle_smt_goal env goal |>
(* Keep the same SMT options if the goals were transformed *)
Expand Down
2 changes: 1 addition & 1 deletion src/typechecker/FStar.TypeChecker.TcTerm.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ let no_inst env = {env with Env.instantiate_imp=false}
let is_eq = function
| Some Equality -> true
| _ -> false
let steps env = [Env.Beta; Env.Eager_unfolding; Env.NoFullNorm]
let steps env = [Env.Beta; Env.Eager_unfolding; Env.NoFullNorm; Env.Exclude Env.Zeta]
let norm env t = N.normalize (steps env) env t
let norm_c env c = N.normalize_comp (steps env) env c
let check_no_escape head_opt env (fvs:list bv) kt : term * guard_t =
Expand Down