Skip to content

Commit

Permalink
Normalizer: another fix for FStarLang#3213
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtzguido
mtzguido committed Feb 12, 2024
1 parent 4659832 commit aea8db8
Show file tree
Hide file tree
Showing 4 changed files with 190 additions and 133 deletions.
284 changes: 157 additions & 127 deletions src/typechecker/FStar.TypeChecker.Normalize.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1154,6 +1154,161 @@ let get_extraction_mode env (m:Ident.lident) =
let can_reify_for_extraction env (m:Ident.lident) =
(get_extraction_mode env m) = S.Extract_reify

(* Checks if a list of arguments matches some binders exactly *)
let rec args_are_binders args bs : bool =
match args, bs with
| (t, _)::args, b::bs ->
begin match (SS.compress t).n with
| Tm_name bv' -> S.bv_eq b.binder_bv bv' && args_are_binders args bs
| _ -> false
end
| [], [] -> true
| _, _ -> false

(* Is t a variable applied to exactly bs? If so return it. *)
let is_applied cfg (bs:binders) (t : term) : option bv =
if cfg.debug.wpe then
BU.print2 "WPE> is_applied %s -- %s\n" (Print.term_to_string t) (Print.tag_of_term t);
let hd, args = U.head_and_args_full t in
match (SS.compress hd).n with
| Tm_name bv when args_are_binders args bs ->
if cfg.debug.wpe then
BU.print3 "WPE> got it\n>>>>top = %s\n>>>>b = %s\n>>>>hd = %s\n"
(Print.term_to_string t)
(Print.bv_to_string bv)
(Print.term_to_string hd);
Some bv
| _ -> None

(* As above accounting for squashes *)
let is_applied_maybe_squashed cfg (bs : binders) (t : term) : option bv =
if cfg.debug.wpe then
BU.print2 "WPE> is_applied_maybe_squashed %s -- %s\n" (Print.term_to_string t) (Print.tag_of_term t);
match is_squash t with
| Some (_, t') -> is_applied cfg bs t'
| _ -> begin match is_auto_squash t with
| Some (_, t') -> is_applied cfg bs t'
| _ -> is_applied cfg bs t
end

let is_quantified_const cfg (bv:bv) (phi : term) : option term =
let open FStar.Syntax.Formula in
let open FStar.Class.Monad in
let guard (b:bool) : option unit = if b then Some () else None in

let phi0 = phi in
let types_match bs =
(* We need to make sure that the forall above is over the same types
as those in the domain of `f`. See bug #3213. *)
let bs_q, _ = !__get_n_binders cfg.tcenv [AllowUnboundUniverses] (List.length bs) bv.sort in
let rec unrefine_true (t:term) : term =
(* Discard trivial refinements. *)
match (SS.compress t).n with
| Tm_refine {b; phi} when U.term_eq phi U.t_true -> unrefine_true b.sort
| _ -> t
in
List.length bs = List.length bs_q &&
List.forall2 (fun b1 b2 ->
let s1 = b1.binder_bv.sort |> unrefine_true in
let s2 = b2.binder_bv.sort |> unrefine_true in
U.term_eq s1 s2)
bs bs_q
in
let is_bv (bv:S.bv) (t:term) =
match (SS.compress t).n with
| Tm_name bv' -> S.bv_eq bv bv'
| _ -> false
in
let replace_full_applications_with (bv:S.bv) (arity:int) (s:term) (t:term) : term & bool =
let chgd = BU.mk_ref false in
let t' = t |> Syntax.Visit.visit_term (fun t ->
let hd, args = U.head_and_args t in
if List.length args = arity && is_bv bv hd then (
chgd := true;
s
) else
t)
in
t', !chgd
in
let! form = destruct_typ_as_formula phi in
match form with
| BaseConn (lid, [(p, _); (q, _)]) when Ident.lid_equals lid PC.imp_lid ->
if cfg.debug.wpe then
BU.print2 "WPE> p = (%s); q = (%s)\n"
(Print.term_to_string p)
(Print.term_to_string q);
let! q' =
begin match destruct_typ_as_formula p with
(* Case 1 *)
| None -> begin match (SS.compress p).n with
| Tm_bvar bv' when S.bv_eq bv bv' ->
if cfg.debug.wpe then
BU.print_string "WPE> Case 1\n";
let q' = SS.subst [NT (bv, U.t_true)] q in
Some q'
| _ -> None
end
(* Case 2 *)
| Some (BaseConn (lid, [(p, _)])) when Ident.lid_equals lid PC.not_lid ->
begin match (SS.compress p).n with
| Tm_bvar bv' when S.bv_eq bv bv' ->
if cfg.debug.wpe then
BU.print_string "WPE> Case 2\n";
let q' = SS.subst [NT (bv, U.t_false)] q in
Some q'
| _ -> None
end
| Some (QAll (bs, pats, phi)) when types_match bs ->
begin match destruct_typ_as_formula phi with
| None ->
let! bv' = is_applied_maybe_squashed cfg bs phi in
guard (S.bv_eq bv bv');!
(* Case 3 *)
if cfg.debug.wpe then
BU.print_string "WPE> Case 3\n";
let q', chgd = replace_full_applications_with bv (List.length bs) U.t_true q in
guard chgd;! (* If nothing triggered, do not rewrite to itself to avoid infinite loops *)
Some q'
| Some (BaseConn (lid, [(p, _)])) when Ident.lid_equals lid PC.not_lid ->
let! bv' = is_applied_maybe_squashed cfg bs p in
guard (S.bv_eq bv bv');!
if cfg.debug.wpe then
BU.print_string "WPE> Case 4\n";
let q', chgd = replace_full_applications_with bv (List.length bs) U.t_false q in
guard chgd;!
Some q'
| _ ->
None
end
| _ -> None
end
in
let phi' = U.mk_app (S.fvar PC.imp_lid None) [S.as_arg p; S.as_arg q'] in
Some phi'
| _ -> None

// A very F*-specific optimization:
// 1) forall f. (f ==> E[f]) ~> E[True]
// 2) forall f. (~f ==> E[f]) ~> E[False]
//
// 3) forall f. (forall j1 ... jn. f j1 ... jn) ==> E
// ~> forall f. (forall j1 ... jn. f j1 ... jn) ==> E', where every full application of `f` to `n` binders is rewritten to true
//
// 4) forall f. (forall j1 ... jn. ~(f j1 ... jn)) ==> E
// ~> forall f. (forall j1 ... jn. ~(f j1 ... jn)) ==> E', idem rewriting to false
// reurns the rewritten formula.
let is_forall_const cfg (phi : term) : option term =
let open FStar.Syntax.Formula in
match Syntax.Formula.destruct_typ_as_formula phi with
| Some (QAll ([b], _, phi')) ->
let open FStar.Class.Monad in
if cfg.debug.wpe then
BU.print2 "WPE> QAll [%s] %s\n" (show b.binder_bv) (show phi');
let! phi' = is_quantified_const cfg b.binder_bv phi' in
Some (U.mk_forall (cfg.tcenv.universe_of cfg.tcenv b.binder_bv.sort) b.binder_bv phi')

| _ -> None

(* GM: Please consider this function private outside of this recursive
* group, and call `normalize` instead. `normalize` will print timing
Expand Down Expand Up @@ -2278,7 +2433,6 @@ and norm_cb cfg : EMB.norm_cb = function
(* The boolean indicates whether further normalization is required. *)
(*******************************************************************)
and maybe_simplify_aux (cfg:cfg) (env:env) (stack:stack) (tm:term) : term & bool =
let open FStar.Syntax.Formula in
let tm, renorm = reduce_primops (norm_cb cfg) cfg env tm in
if not <| cfg.steps.simplify then tm, renorm
else
Expand All @@ -2290,130 +2444,6 @@ and maybe_simplify_aux (cfg:cfg) (env:env) (stack:stack) (tm:term) : term & bool
| Tm_fvar fv when S.fv_eq_lid fv PC.false_lid -> Some false
| _ -> None
in
let rec args_are_binders args bs =
match args, bs with
| (t, _)::args, b::bs ->
begin match (SS.compress t).n with
| Tm_name bv' -> S.bv_eq b.binder_bv bv' && args_are_binders args bs
| _ -> false
end
| [], [] -> true
| _, _ -> false
in
let is_applied (bs:binders) (t : term) : option bv =
if cfg.debug.wpe then
BU.print2 "WPE> is_applied %s -- %s\n" (Print.term_to_string t) (Print.tag_of_term t);
let hd, args = U.head_and_args_full t in
match (SS.compress hd).n with
| Tm_name bv when args_are_binders args bs ->
if cfg.debug.wpe then
BU.print3 "WPE> got it\n>>>>top = %s\n>>>>b = %s\n>>>>hd = %s\n"
(Print.term_to_string t)
(Print.bv_to_string bv)
(Print.term_to_string hd);
Some bv
| _ -> None
in
let is_applied_maybe_squashed (bs : binders) (t : term) : option bv =
if cfg.debug.wpe then
BU.print2 "WPE> is_applied_maybe_squashed %s -- %s\n" (Print.term_to_string t) (Print.tag_of_term t);
match is_squash t with
| Some (_, t') -> is_applied bs t'
| _ -> begin match is_auto_squash t with
| Some (_, t') -> is_applied bs t'
| _ -> is_applied bs t
end
in
// A very F*-specific optimization:
// 1) forall p. (p ==> E[p]) ~> E[True]
// 2) forall p. (~p ==> E[p]) ~> E[False]
// 3) forall p. (forall j1 j2 ... jn. p j1 j2 ... jn) ==> E[p] ~> E[(fun j1 j2 ... jn -> True)]
// 4) forall p. (forall j1 j2 ... jn. ~(p j1 j2 ... jn)) ==> E[p] ~> E[(fun j1 j2 ... jn -> False)]
let is_quantified_const (bv:bv) (phi : term) : option term =
let open FStar.Syntax.Formula in
let types_match bs =
(* We need to make sure that the forall above is over the same types
as those in the domain of `f`. See bug #3213. *)
let bs_q, _ = !__get_n_binders cfg.tcenv [AllowUnboundUniverses] (List.length bs) bv.sort in
let rec unrefine_true (t:term) : term =
(* Discard trivial refinements. *)
match (SS.compress t).n with
| Tm_refine {b; phi} when U.term_eq phi U.t_true -> unrefine_true b.sort
| _ -> t
in
List.length bs = List.length bs_q &&
List.forall2 (fun b1 b2 ->
let s1 = b1.binder_bv.sort |> unrefine_true in
let s2 = b2.binder_bv.sort |> unrefine_true in
U.term_eq s1 s2)
bs bs_q
in
match destruct_typ_as_formula phi with
| Some (BaseConn (lid, [(p, _); (q, _)])) when Ident.lid_equals lid PC.imp_lid ->
if cfg.debug.wpe then
BU.print2 "WPE> p = (%s); q = (%s)\n"
(Print.term_to_string p)
(Print.term_to_string q);
begin match destruct_typ_as_formula p with
// Case 1)
| None -> begin match (SS.compress p).n with
| Tm_bvar bv' when S.bv_eq bv bv' ->
if cfg.debug.wpe then
BU.print_string "WPE> Case 1\n";
Some (SS.subst [NT (bv, U.t_true)] q)
| _ -> None
end

// Case 2)
| Some (BaseConn (lid, [(p, _)])) when Ident.lid_equals lid PC.not_lid ->
begin match (SS.compress p).n with
| Tm_bvar bv' when S.bv_eq bv bv' ->
if cfg.debug.wpe then
BU.print_string "WPE> Case 2\n";
Some (SS.subst [NT (bv, U.t_false)] q)
| _ -> None
end

| Some (QAll (bs, pats, phi)) when types_match bs ->
begin match destruct_typ_as_formula phi with
| None ->
begin match is_applied_maybe_squashed bs phi with
// Case 3)
| Some bv' when S.bv_eq bv bv' ->
if cfg.debug.wpe then
BU.print_string "WPE> Case 3\n";
let ftrue = U.abs bs U.t_true (Some (U.residual_tot U.ktype0)) in
Some (SS.subst [NT (bv, ftrue)] q)
| _ ->
None
end
| Some (BaseConn (lid, [(p, _)])) when Ident.lid_equals lid PC.not_lid ->
begin match is_applied_maybe_squashed bs p with
// Case 4)
| Some bv' when S.bv_eq bv bv' ->
if cfg.debug.wpe then
BU.print_string "WPE> Case 4\n";
let ffalse = U.abs bs U.t_false (Some (U.residual_tot U.ktype0)) in
Some (SS.subst [NT (bv, ffalse)] q)
| _ ->
None
end
| _ ->
None
end

| _ -> None
end
| _ -> None
in
let is_forall_const (phi : term) : option term =
match destruct_typ_as_formula phi with
| Some (QAll ([b], _, phi')) ->
if cfg.debug.wpe then
BU.print2 "WPE> QAll [%s] %s\n" (Print.bv_to_string b.binder_bv) (Print.term_to_string phi');
is_quantified_const b.binder_bv phi'
| _ -> None
in
let is_const_match (phi : term) : option bool =
match (SS.compress phi).n with
(* Trying to be efficient, but just checking if they all agree *)
Expand Down Expand Up @@ -2465,11 +2495,11 @@ and maybe_simplify_aux (cfg:cfg) (env:env) (stack:stack) (tm:term) : term & bool
| _ -> false
in
let simplify arg = (simp_t (fst arg), arg) in
match is_forall_const tm with
match is_forall_const cfg tm with
(* We need to recurse, and maybe reduce further! *)
| Some tm' ->
if cfg.debug.wpe then
BU.print2 "WPE> %s ~> %s\n" (Print.term_to_string tm) (Print.term_to_string tm');
BU.print2 "WPE> %s ~> %s\n" (show tm) (show tm');
maybe_simplify_aux cfg env stack (norm cfg env [] tm')
(* Otherwise try to simplify this point *)
| None ->
Expand Down
7 changes: 2 additions & 5 deletions tests/bug-reports/Bug3213.fst
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module Bug3213

let this_is_ok ()
: Lemma (forall (f : (nat -> Type0)). (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) = ()
let forall_elim (#a: Type) (p: (a -> GTot Type)) (x:a)
: Lemma (requires forall (x: a). p x) (ensures p x) = ()

[@@expect_failure [19]]
let bad ()
Expand All @@ -11,9 +11,6 @@ let bad ()
let bad_assumed ()
: Lemma (forall (f : int -> Type0). (forall (x : nat). f x) ==> f (-1)) = admit()

let forall_elim (#a: Type) (p: (a -> GTot Type)) (x:a)
: Lemma (requires forall (x: a). p x) (ensures p x) = ()

let falso () : Lemma False =
bad_assumed();
let f (x:int) : Type0 = x >= 0 in
Expand Down
30 changes: 30 additions & 0 deletions tests/bug-reports/Bug3213b.fst
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
module Bug3213b

let forall_elim (#a: Type) (p: (a -> GTot Type)) (x:a)
: Lemma (requires forall (x: a). p x) (ensures p x) = ()

[@@expect_failure [19]]
let also_bad ()
: Lemma (forall (f : (nat -> Type0)). (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) = ()

let also_bad_assumed ()
: Lemma (forall (f : (nat -> Type0)). (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) = admit()

let eq_fun (f1 f2 : 'a -> 'b) (x : 'a) (_ : squash (f1 == f2)) : Lemma (f1 x == f2 x) = ()

let bad2 () =
let f0 : int -> Type0 = fun x -> True in
let f1 : int -> Type0 = fun x -> x >= 0 in
also_bad_assumed ();
let f0' : nat -> Type0 = f0 in
let f1' : nat -> Type0 = f1 in
forall_elim #(nat -> Type0) (fun f -> (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) f0';
forall_elim #(nat -> Type0) (fun f -> (forall (x : nat). f x) ==> (fun (_:nat) -> True) == f) f1';
assert (f0' == (fun (_:nat) -> True));
assert (f1' == (fun (_:nat) -> True));
assert (eq2 #(nat -> Type0) f0' f0);
assert (eq2 #(nat -> Type0) f1' f1);
assert (f0 == f1);
eq_fun f0 f1 (-1) ();
assert False;
()
2 changes: 1 addition & 1 deletion tests/bug-reports/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \
Bug2415.fst Bug3028.fst Bug2954.fst Bug3089.fst Bug3102.fst Bug2981.fst Bug2980.fst Bug3115.fst \
Bug2083.fst Bug2002.fst Bug1482.fst Bug1066.fst Bug3120a.fst Bug3120b.fst Bug3186.fst Bug3185.fst Bug3210.fst \
Bug3213.fst
Bug3213.fst Bug3213b.fst

SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst
Expand Down

0 comments on commit aea8db8

Please sign in to comment.