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

Revising equality check in Core to emit a guard #2971

Merged
merged 4 commits into from
Jun 26, 2023
Merged

Revising equality check in Core to emit a guard #2971

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
35e5c5d
revising equality check in Core to emit a guard in case head symbols …
nikswamy Jun 20, 2023
43dedd2
Merge remote-tracking branch 'origin/master' into _nik_core_equatable
nikswamy Jun 23, 2023
2dfd8d7
revise check to first proceed structurally without guard, and then fa…
nikswamy Jun 23, 2023
bc78630
Merge remote-tracking branch 'origin/master' into _nik_core_equatable
nikswamy Jun 26, 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
196 changes: 121 additions & 75 deletions ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
View file
Open in desktop

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

28 changes: 21 additions & 7 deletions src/typechecker/FStar.TypeChecker.Core.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -825,13 +825,16 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ)
: option (term & term)
= maybe_unfold_side (which_side_to_unfold t0 t1) t0 t1
in
let emit_guard t0 t1 =
let! _, t_typ = check' g t0 in
let! u = universe_of g t_typ in
guard (U.mk_eq2 u t_typ t0 t1)
in
let fallback t0 t1 =
if guard_ok
then if equatable g t0
|| equatable g t1
then let! _, t_typ = check' g t0 in
let! u = universe_of g t_typ in
guard (U.mk_eq2 u t_typ t0 t1)
then emit_guard t0 t1
else err ()
else err ()
in
Expand Down Expand Up @@ -1002,10 +1005,21 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ)
if not (head_matches && List.length args0 = List.length args1)
then maybe_unfold_and_retry t0 t1
else (
handle_with
(check_relation g EQUALITY head0 head1 ;!
check_relation_args g EQUALITY args0 args1)
(fun _ -> maybe_unfold_side_and_retry Both t0 t1)
(* If we're proving equality and SMT queries are ok,
defer things like `v.v1 == u.v1` to SMT
rather than matching on the v1 projector and
trying to prove `v == u` *)
if guard_ok &&
(rel=EQUALITY) &&
equatable g t0 &&
nikswamy marked this conversation as resolved.
Show resolved Hide resolved
equatable g t1
then emit_guard t0 t1
else (
handle_with
(check_relation g EQUALITY head0 head1 ;!
check_relation_args g EQUALITY args0 args1)
(fun _ -> maybe_unfold_side_and_retry Both t0 t1)
)
)

| Tm_abs {bs=b0::b1::bs; body; rc_opt=ropt}, _ ->
Expand Down