From 15a8977177c7ac9639a099e2a1e88b4eeb86ef0f Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sat, 28 Sep 2024 17:08:05 -0700 Subject: [PATCH] an option to retain old prop typing; fix a regression test that instantiates existential quanitifers "magically" --- .../generated/FStar_SMTEncoding_Encode.ml | 54 +++++++++++-------- src/smtencoding/FStar.SMTEncoding.Encode.fst | 2 +- src/smtencoding/FStar.SMTEncoding.Pruning.fst | 4 ++ tests/bug-reports/Bug2172.fst | 7 +-- 4 files changed, 38 insertions(+), 29 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml index 536252f940c..0e5e30d67ee 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml @@ -2967,74 +2967,82 @@ let (encode_top_level_let : if should_encode_logical then - (if - is_sub_singleton + let uu___17 = + is_sub_singleton + && + (let uu___18 + = + FStar_Options_Ext.get + "retain_old_prop_typing" in + uu___18 = + "") in + (if uu___17 then - let uu___17 + let uu___18 = - let uu___18 - = - let uu___19 + let uu___19 = let uu___20 = - FStar_Syntax_Syntax.range_of_lbname - lbn in let uu___21 = + FStar_Syntax_Syntax.range_of_lbname + lbn in let uu___22 = + let uu___23 + = FStar_SMTEncoding_Term.mk_Valid app_is_prop in ([ [app_is_prop]], vars1, - uu___22) in + uu___23) in FStar_SMTEncoding_Term.mkForall - uu___20 - uu___21 in - let uu___20 - = + uu___21 + uu___22 in let uu___21 = let uu___22 = + let uu___23 + = FStar_Ident.string_of_lid flid in FStar_Compiler_Util.format1 "Prop-typing for %s" - uu___22 in + uu___23 in FStar_Pervasives_Native.Some - uu___21 in - (uu___19, - uu___20, + uu___22 in + (uu___20, + uu___21, (Prims.strcat basic_eqn_name (Prims.strcat "_" fvb.FStar_SMTEncoding_Env.smt_id))) in FStar_SMTEncoding_Util.mkAssume - uu___18 in - (uu___17, + uu___19 in + (uu___18, []) else - (let uu___18 + (let uu___19 = FStar_SMTEncoding_EncodeTerm.encode_term body env'1 in - match uu___18 + match uu___19 with | (body1, decls2) -> - let uu___19 + let uu___20 = make_eqn basic_eqn_name app_is_prop app body1 in - (uu___19, + (uu___20, decls2))) else (let uu___18 = diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fst b/src/smtencoding/FStar.SMTEncoding.Encode.fst index 437042ad44e..3c618468334 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fst @@ -821,7 +821,7 @@ let encode_top_level_let : let app_is_prop = Term.mk_subtype_of_unit app in if should_encode_logical then ( - if is_sub_singleton + if is_sub_singleton && Options.Ext.get "retain_old_prop_typing" = "" then ( Util.mkAssume(mkForall (S.range_of_lbname lbn) ([[app_is_prop]], vars, mk_Valid <| app_is_prop), diff --git a/src/smtencoding/FStar.SMTEncoding.Pruning.fst b/src/smtencoding/FStar.SMTEncoding.Pruning.fst index 4070a4a8cda..b58bcfc7f73 100644 --- a/src/smtencoding/FStar.SMTEncoding.Pruning.fst +++ b/src/smtencoding/FStar.SMTEncoding.Pruning.fst @@ -461,4 +461,8 @@ let prune (p:pruning_state) (roots:list decl) | Some a -> [a]) (reached_names@p.ambients) in + // if Options.Ext.get "debug_context_pruning" <> "" + // then ( + // BU.print1 "Retained %s assumptions\n" (show (List.length reached_assumptions)) + // ); reached_assumptions \ No newline at end of file diff --git a/tests/bug-reports/Bug2172.fst b/tests/bug-reports/Bug2172.fst index b126ac1948a..3fca4c384ca 100644 --- a/tests/bug-reports/Bug2172.fst +++ b/tests/bug-reports/Bug2172.fst @@ -1,14 +1,11 @@ module Bug2172 #push-options "--ext context_pruning" // one existential quantification over two variables (`p2` below) is -// different from two extistential quantifications over one variable +// different from two existential quantifications over one variable // each (`p1` below) let p1 = exists (x: int). exists (y: int). 0 == x + y let p2 = exists (x: int) (y: int). 0 == x + y let test0 (witness:nat) = assert p1 -#pop-options -#push-options "--ext 'context_pruning='" -let test1 = assert p2 -#pop-options +let test1 (x:int) = assert (0 == x + (-x)); assert p2 let _ = assert (p1 <==> p2)