diff --git a/ocaml/fstar-lib/FStar_Tactics_V1_Builtins.ml b/ocaml/fstar-lib/FStar_Tactics_V1_Builtins.ml index b121dfd2d1e..f326735c12b 100644 --- a/ocaml/fstar-lib/FStar_Tactics_V1_Builtins.ml +++ b/ocaml/fstar-lib/FStar_Tactics_V1_Builtins.ml @@ -142,10 +142,3 @@ let ctrl_rewrite (t2 : unit -> unit __tac) : unit __tac = from_tac_3 CTRW.ctrl_rewrite d (to_tac_1 t1) (to_tac_0 (t2 ())) - -let log_issues (i:FStar_Issue.issue list) - : unit __tac - = fun ps -> - FStar_Errors.add_many i; - FStar_Tactics_Result.Success ((), ps) - diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml index 668af33f931..65d2f03d4fe 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml @@ -7741,7 +7741,20 @@ let (encode_query : uu___11 in FStar_SMTEncoding_Term.Caption uu___10 in - [uu___9] + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = + FStar_Errors.get_ctx () in + FStar_String.concat "\n" + uu___14 in + Prims.op_Hat "Context: " + uu___13 in + FStar_SMTEncoding_Term.Caption + uu___12 in + [uu___11] in + uu___9 :: uu___10 else [] in let query_prelude = let uu___8 = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index 3c5057eb3a3..75a02db4ef9 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -2040,28 +2040,44 @@ let (split_and_solve : fun use_env_msg -> fun tcenv -> fun q -> - let goals = - let uu___ = FStar_TypeChecker_Env.split_smt_query tcenv q in - match uu___ with - | FStar_Pervasives_Native.None -> - failwith "Impossible: split_query callback is not set" - | FStar_Pervasives_Native.Some goals1 -> goals1 in - FStar_Compiler_Effect.op_Bar_Greater goals - (FStar_Compiler_List.iter - (fun uu___1 -> - match uu___1 with - | (env, goal) -> - do_solve false retrying use_env_msg env goal)); - (let uu___1 = - (let uu___2 = FStar_Errors.get_err_count () in - uu___2 = Prims.int_zero) && retrying in - if uu___1 - then - FStar_TypeChecker_Err.log_issue tcenv - tcenv.FStar_TypeChecker_Env.range - (FStar_Errors_Codes.Warning_SplitAndRetryQueries, - "The verification condition succeeded after splitting it to localize potential errors, although the original non-split verification condition failed. If you want to rely on splitting queries for verifying your program please use the '--split_queries always' option rather than relying on it implicitly.") - else ()) + let uu___ = FStar_Options.query_stats () in + if uu___ + then + let range = + let uu___1 = + let uu___2 = + let uu___3 = FStar_TypeChecker_Env.get_range tcenv in + FStar_Compiler_Range_Ops.string_of_range uu___3 in + Prims.op_Hat uu___2 ")" in + Prims.op_Hat "(" uu___1 in + (FStar_Compiler_Util.print2 + "%s\tQuery-stats splitting query because %s\n" range + (if retrying + then "retrying failed query" + else "--split_queries is always"); + (let goals = + let uu___2 = FStar_TypeChecker_Env.split_smt_query tcenv q in + match uu___2 with + | FStar_Pervasives_Native.None -> + failwith "Impossible: split_query callback is not set" + | FStar_Pervasives_Native.Some goals1 -> goals1 in + FStar_Compiler_Effect.op_Bar_Greater goals + (FStar_Compiler_List.iter + (fun uu___3 -> + match uu___3 with + | (env, goal) -> + do_solve false retrying use_env_msg env goal)); + (let uu___3 = + (let uu___4 = FStar_Errors.get_err_count () in + uu___4 = Prims.int_zero) && retrying in + if uu___3 + then + FStar_TypeChecker_Err.log_issue tcenv + tcenv.FStar_TypeChecker_Env.range + (FStar_Errors_Codes.Warning_SplitAndRetryQueries, + "The verification condition succeeded after splitting it to localize potential errors, although the original non-split verification condition failed. If you want to rely on splitting queries for verifying your program please use the '--split_queries always' option rather than relying on it implicitly.") + else ()))) + else () let disable_quake_for : 'a . (unit -> 'a) -> 'a = fun f -> FStar_Options.with_saved_options diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml index 84374eb07d7..7e24d360623 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml @@ -83,6 +83,8 @@ let (fstar_tactics_tot_or_ghost_EGhost : tac_constant) = let (fstar_tactics_guard_policy : tac_constant) = fstar_tactics_const ["Types"; "guard_policy"] let (fstar_tactics_SMT : tac_constant) = fstar_tactics_data ["Types"; "SMT"] +let (fstar_tactics_SMTSync : tac_constant) = + fstar_tactics_data ["Types"; "SMTSync"] let (fstar_tactics_Goal : tac_constant) = fstar_tactics_data ["Types"; "Goal"] let (fstar_tactics_Drop : tac_constant) = @@ -831,6 +833,7 @@ let (e_guard_policy : let embed_guard_policy rng p = match p with | FStar_Tactics_Types.SMT -> fstar_tactics_SMT.t + | FStar_Tactics_Types.SMTSync -> fstar_tactics_SMTSync.t | FStar_Tactics_Types.Goal -> fstar_tactics_Goal.t | FStar_Tactics_Types.Force -> fstar_tactics_Force.t | FStar_Tactics_Types.Drop -> fstar_tactics_Drop.t in @@ -842,6 +845,9 @@ let (e_guard_policy : | FStar_Syntax_Syntax.Tm_fvar fv when FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_SMT.lid -> FStar_Pervasives_Native.Some FStar_Tactics_Types.SMT + | FStar_Syntax_Syntax.Tm_fvar fv when + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_SMTSync.lid -> + FStar_Pervasives_Native.Some FStar_Tactics_Types.SMTSync | FStar_Syntax_Syntax.Tm_fvar fv when FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_Goal.lid -> FStar_Pervasives_Native.Some FStar_Tactics_Types.Goal @@ -858,6 +864,8 @@ let (e_guard_policy_nbe : let embed_guard_policy cb p = match p with | FStar_Tactics_Types.SMT -> mkConstruct fstar_tactics_SMT.fv [] [] + | FStar_Tactics_Types.SMTSync -> + mkConstruct fstar_tactics_SMTSync.fv [] [] | FStar_Tactics_Types.Goal -> mkConstruct fstar_tactics_Goal.fv [] [] | FStar_Tactics_Types.Force -> mkConstruct fstar_tactics_Force.fv [] [] | FStar_Tactics_Types.Drop -> mkConstruct fstar_tactics_Drop.fv [] [] in @@ -867,6 +875,9 @@ let (e_guard_policy_nbe : | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_SMT.lid -> FStar_Pervasives_Native.Some FStar_Tactics_Types.SMT + | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_SMTSync.lid -> + FStar_Pervasives_Native.Some FStar_Tactics_Types.SMTSync | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_Goal.lid -> FStar_Pervasives_Native.Some FStar_Tactics_Types.Goal diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml index 03982dbf46a..d5647e3e4c3 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml @@ -33,12 +33,15 @@ let (__proj__Mkgoal__item__label : goal -> Prims.string) = type guard_policy = | Goal | SMT + | SMTSync | Force | Drop let (uu___is_Goal : guard_policy -> Prims.bool) = fun projectee -> match projectee with | Goal -> true | uu___ -> false let (uu___is_SMT : guard_policy -> Prims.bool) = fun projectee -> match projectee with | SMT -> true | uu___ -> false +let (uu___is_SMTSync : guard_policy -> Prims.bool) = + fun projectee -> match projectee with | SMTSync -> true | uu___ -> false let (uu___is_Force : guard_policy -> Prims.bool) = fun projectee -> match projectee with | Force -> true | uu___ -> false let (uu___is_Drop : guard_policy -> Prims.bool) = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml index b972a64fefd..dd092f57225 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml @@ -498,10 +498,10 @@ let (proc_guard' : FStar_Tactics_Monad.mlog (fun uu___4 -> let uu___5 = - FStar_TypeChecker_Rel.guard_to_string - e g in + FStar_Syntax_Print.term_to_string + f in FStar_Compiler_Util.print2 - "Sending guard (%s:%s) to SMT goal\n" + "Pushing guard (%s:%s) as SMT goal\n" reason uu___5) (fun uu___4 -> let uu___5 = @@ -512,6 +512,19 @@ let (proc_guard' : (fun g1 -> FStar_Tactics_Monad.push_smt_goals [g1])) + | FStar_Tactics_Types.SMTSync -> + FStar_Tactics_Monad.mlog + (fun uu___4 -> + let uu___5 = + FStar_Syntax_Print.term_to_string + f in + FStar_Compiler_Util.print2 + "Sending guard (%s:%s) to SMT Synchronously\n" + reason uu___5) + (fun uu___4 -> + FStar_TypeChecker_Rel.force_trivial_guard + e g; + FStar_Tactics_Monad.ret ()) | FStar_Tactics_Types.Force -> FStar_Tactics_Monad.mlog (fun uu___4 -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index 77d1b66f81c..bda9f2e15a6 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -418,6 +418,129 @@ let with_policy : let uu___3 = set_guard_policy old_pol in FStar_Tactics_Monad.bind uu___3 (fun uu___4 -> FStar_Tactics_Monad.ret r)))) +let (proc_guard_formula : + Prims.string -> + env -> + FStar_Syntax_Syntax.term -> + FStar_Syntax_Syntax.should_check_uvar FStar_Pervasives_Native.option + -> FStar_Compiler_Range_Type.range -> unit FStar_Tactics_Monad.tac) + = + fun reason -> + fun e -> + fun f -> + fun sc_opt -> + fun rng -> + FStar_Tactics_Monad.op_let_Bang FStar_Tactics_Monad.get + (fun ps -> + match ps.FStar_Tactics_Types.guard_policy with + | FStar_Tactics_Types.Drop -> + ((let uu___1 = + let uu___2 = + let uu___3 = FStar_Syntax_Print.term_to_string f in + FStar_Compiler_Util.format1 + "Tactics admitted guard <%s>\n\n" uu___3 in + (FStar_Errors_Codes.Warning_TacAdmit, uu___2) in + FStar_Errors.log_issue e.FStar_TypeChecker_Env.range + uu___1); + FStar_Tactics_Monad.ret ()) + | FStar_Tactics_Types.Goal -> + FStar_Tactics_Monad.mlog + (fun uu___ -> + let uu___1 = FStar_Syntax_Print.term_to_string f in + FStar_Compiler_Util.print2 + "Making guard (%s:%s) into a goal\n" reason + uu___1) + (fun uu___ -> + let uu___1 = + FStar_Tactics_Monad.goal_of_guard reason e f + sc_opt rng in + FStar_Tactics_Monad.op_let_Bang uu___1 + (fun g -> FStar_Tactics_Monad.push_goals [g])) + | FStar_Tactics_Types.SMT -> + FStar_Tactics_Monad.mlog + (fun uu___ -> + let uu___1 = FStar_Syntax_Print.term_to_string f in + FStar_Compiler_Util.print2 + "Pushing guard (%s:%s) as SMT goal\n" reason + uu___1) + (fun uu___ -> + let uu___1 = + FStar_Tactics_Monad.goal_of_guard reason e f + sc_opt rng in + FStar_Tactics_Monad.op_let_Bang uu___1 + (fun g -> FStar_Tactics_Monad.push_smt_goals [g])) + | FStar_Tactics_Types.SMTSync -> + FStar_Tactics_Monad.mlog + (fun uu___ -> + let uu___1 = FStar_Syntax_Print.term_to_string f in + FStar_Compiler_Util.print2 + "Sending guard (%s:%s) to SMT Synchronously\n" + reason uu___1) + (fun uu___ -> + let g = + { + FStar_TypeChecker_Common.guard_f = + (FStar_TypeChecker_Common.NonTrivial f); + FStar_TypeChecker_Common.deferred_to_tac = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); + FStar_TypeChecker_Common.deferred = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); + FStar_TypeChecker_Common.univ_ineqs = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); + FStar_TypeChecker_Common.implicits = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) + } in + FStar_TypeChecker_Rel.force_trivial_guard e g; + FStar_Tactics_Monad.ret ()) + | FStar_Tactics_Types.Force -> + FStar_Tactics_Monad.mlog + (fun uu___ -> + let uu___1 = FStar_Syntax_Print.term_to_string f in + FStar_Compiler_Util.print2 + "Forcing guard (%s:%s)\n" reason uu___1) + (fun uu___ -> + let g = + { + FStar_TypeChecker_Common.guard_f = + (FStar_TypeChecker_Common.NonTrivial f); + FStar_TypeChecker_Common.deferred_to_tac = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); + FStar_TypeChecker_Common.deferred = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.deferred); + FStar_TypeChecker_Common.univ_ineqs = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.univ_ineqs); + FStar_TypeChecker_Common.implicits = + (FStar_TypeChecker_Env.trivial_guard.FStar_TypeChecker_Common.implicits) + } in + try + (fun uu___1 -> + match () with + | () -> + let uu___2 = + let uu___3 = + let uu___4 = + FStar_TypeChecker_Rel.discharge_guard_no_smt + e g in + FStar_Compiler_Effect.op_Less_Bar + FStar_TypeChecker_Env.is_trivial + uu___4 in + Prims.op_Negation uu___3 in + if uu___2 + then + fail1 "Forcing the guard failed (%s)" + reason + else FStar_Tactics_Monad.ret ()) () + with + | uu___1 -> + FStar_Tactics_Monad.mlog + (fun uu___2 -> + let uu___3 = + FStar_Syntax_Print.term_to_string f in + FStar_Compiler_Util.print1 "guard = %s\n" + uu___3) + (fun uu___2 -> + fail1 "Forcing the guard failed (%s)" + reason))) let (proc_guard' : Prims.bool -> Prims.string -> @@ -465,116 +588,7 @@ let (proc_guard' : | FStar_TypeChecker_Common.Trivial -> FStar_Tactics_Monad.ret () | FStar_TypeChecker_Common.NonTrivial f -> - FStar_Tactics_Monad.op_let_Bang - FStar_Tactics_Monad.get - (fun ps -> - match ps.FStar_Tactics_Types.guard_policy - with - | FStar_Tactics_Types.Drop -> - ((let uu___5 = - let uu___6 = - let uu___7 = - FStar_TypeChecker_Rel.guard_to_string - e g in - FStar_Compiler_Util.format1 - "Tactics admitted guard <%s>\n\n" - uu___7 in - (FStar_Errors_Codes.Warning_TacAdmit, - uu___6) in - FStar_Errors.log_issue - e.FStar_TypeChecker_Env.range - uu___5); - FStar_Tactics_Monad.ret ()) - | FStar_Tactics_Types.Goal -> - FStar_Tactics_Monad.mlog - (fun uu___4 -> - let uu___5 = - FStar_TypeChecker_Rel.guard_to_string - e g in - FStar_Compiler_Util.print2 - "Making guard (%s:%s) into a goal\n" - reason uu___5) - (fun uu___4 -> - let uu___5 = - FStar_Tactics_Monad.goal_of_guard - reason e f sc_opt rng in - FStar_Tactics_Monad.op_let_Bang - uu___5 - (fun g1 -> - FStar_Tactics_Monad.push_goals - [g1])) - | FStar_Tactics_Types.SMT -> - FStar_Tactics_Monad.mlog - (fun uu___4 -> - let uu___5 = - FStar_TypeChecker_Rel.guard_to_string - e g in - FStar_Compiler_Util.print2 - "Sending guard (%s:%s) to SMT goal\n" - reason uu___5) - (fun uu___4 -> - let uu___5 = - FStar_Tactics_Monad.goal_of_guard - reason e f sc_opt rng in - FStar_Tactics_Monad.op_let_Bang - uu___5 - (fun g1 -> - FStar_Tactics_Monad.push_smt_goals - [g1])) - | FStar_Tactics_Types.Force -> - FStar_Tactics_Monad.mlog - (fun uu___4 -> - let uu___5 = - FStar_TypeChecker_Rel.guard_to_string - e g in - FStar_Compiler_Util.print2 - "Forcing guard (%s:%s)\n" reason - uu___5) - (fun uu___4 -> - try - (fun uu___5 -> - match () with - | () -> - let uu___6 = - let uu___7 = - let uu___8 = - FStar_TypeChecker_Rel.discharge_guard_no_smt - e g in - FStar_Compiler_Effect.op_Less_Bar - FStar_TypeChecker_Env.is_trivial - uu___8 in - Prims.op_Negation - uu___7 in - if uu___6 - then - FStar_Tactics_Monad.mlog - (fun uu___7 -> - let uu___8 = - FStar_TypeChecker_Rel.guard_to_string - e g in - FStar_Compiler_Util.print1 - "guard = %s\n" - uu___8) - (fun uu___7 -> - fail1 - "Forcing the guard failed (%s)" - reason) - else - FStar_Tactics_Monad.ret - ()) () - with - | uu___5 -> - FStar_Tactics_Monad.mlog - (fun uu___6 -> - let uu___7 = - FStar_TypeChecker_Rel.guard_to_string - e g in - FStar_Compiler_Util.print1 - "guard = %s\n" uu___7) - (fun uu___6 -> - fail1 - "Forcing the guard failed (%s)" - reason)))))) + proc_guard_formula reason e f sc_opt rng))) let (proc_guard : Prims.string -> env -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml index e2b24be28ab..d17cafb60aa 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml @@ -3070,9 +3070,7 @@ let run_tactic_on_ps' : FStar_Tactics_Printing.do_dump_proofstate ps2 "at the finish line" else ()); - ((FStar_Compiler_List.op_At - ps2.FStar_Tactics_Types.goals - ps2.FStar_Tactics_Types.smt_goals), ret)))) + (remaining_smt_goals, ret)))) | FStar_Tactics_Result.Failed (e, ps2) -> (FStar_Tactics_Printing.do_dump_proofstate ps2 "at the time of failure"; diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fst b/src/smtencoding/FStar.SMTEncoding.Encode.fst index 4bb5e9412f4..2c66ffe6434 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fst @@ -1944,7 +1944,8 @@ let encode_query use_env_msg (tcenv:Env.env) (q:S.term) let label_prefix, label_suffix = encode_labels labels in let caption = if Options.log_queries () - then [Caption ("Encoding query formula : " ^ (Print.term_to_string q))] + then [Caption ("Encoding query formula : " ^ (Print.term_to_string q)); + Caption ("Context: " ^ String.concat "\n" (Errors.get_ctx ()))] else [] in let query_prelude = diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst index 86ee1e1725f..32bb0cb8e57 100644 --- a/src/smtencoding/FStar.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst @@ -1183,6 +1183,11 @@ let do_solve (can_split:bool) (is_retry:bool) use_env_msg tcenv q : unit = | None -> () (* already logged an error *) let split_and_solve (retrying:bool) use_env_msg tcenv q : unit = + if Options.query_stats () then + let range = "(" ^ (Range.string_of_range (Env.get_range tcenv)) ^ ")" in + BU.print2 "%s\tQuery-stats splitting query because %s\n" + range + (if retrying then "retrying failed query" else "--split_queries is always"); let goals = match Env.split_smt_query tcenv q with | None -> diff --git a/src/tactics/FStar.Tactics.Embedding.fst b/src/tactics/FStar.Tactics.Embedding.fst index e87a461e7ff..2a37858d4f6 100644 --- a/src/tactics/FStar.Tactics.Embedding.fst +++ b/src/tactics/FStar.Tactics.Embedding.fst @@ -98,6 +98,7 @@ let fstar_tactics_tot_or_ghost_EGhost = fstar_tactics_data ["Types"; "E_Ghost"] let fstar_tactics_guard_policy = fstar_tactics_const ["Types"; "guard_policy"] let fstar_tactics_SMT = fstar_tactics_data ["Types"; "SMT"] +let fstar_tactics_SMTSync = fstar_tactics_data ["Types"; "SMTSync"] let fstar_tactics_Goal = fstar_tactics_data ["Types"; "Goal"] let fstar_tactics_Drop = fstar_tactics_data ["Types"; "Drop"] let fstar_tactics_Force = fstar_tactics_data ["Types"; "Force"] @@ -476,6 +477,7 @@ let e_guard_policy = let embed_guard_policy (rng:Range.range) (p : guard_policy) : term = match p with | SMT -> fstar_tactics_SMT.t + | SMTSync -> fstar_tactics_SMTSync.t | Goal -> fstar_tactics_Goal.t | Force -> fstar_tactics_Force.t | Drop -> fstar_tactics_Drop.t @@ -483,6 +485,7 @@ let e_guard_policy = let unembed_guard_policy (t : term) : option guard_policy = match (SS.compress t).n with | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_SMT.lid -> Some SMT + | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_SMTSync.lid -> Some SMTSync | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_Goal.lid -> Some Goal | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_Force.lid -> Some Force | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_Drop.lid -> Some Drop @@ -494,6 +497,7 @@ let e_guard_policy_nbe = let embed_guard_policy cb (p:guard_policy) : NBET.t = match p with | SMT -> mkConstruct fstar_tactics_SMT.fv [] [] + | SMTSync -> mkConstruct fstar_tactics_SMTSync.fv [] [] | Goal -> mkConstruct fstar_tactics_Goal.fv [] [] | Force -> mkConstruct fstar_tactics_Force.fv [] [] | Drop -> mkConstruct fstar_tactics_Drop.fv [] [] @@ -501,6 +505,7 @@ let e_guard_policy_nbe = let unembed_guard_policy cb (t:NBET.t) : option guard_policy = match NBETerm.nbe_t_of_t t with | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_SMT.lid -> Some SMT + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_SMTSync.lid -> Some SMTSync | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_Goal.lid -> Some Goal | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_Force.lid -> Some Force | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_Drop.lid -> Some Drop diff --git a/src/tactics/FStar.Tactics.Types.fsti b/src/tactics/FStar.Tactics.Types.fsti index 3e0a34265dc..6e7121e0f98 100644 --- a/src/tactics/FStar.Tactics.Types.fsti +++ b/src/tactics/FStar.Tactics.Types.fsti @@ -48,6 +48,7 @@ type goal = { type guard_policy = | Goal | SMT + | SMTSync | Force | Drop // unsound diff --git a/src/tactics/FStar.Tactics.V1.Basic.fst b/src/tactics/FStar.Tactics.V1.Basic.fst index b37d077e159..bd07770f062 100644 --- a/src/tactics/FStar.Tactics.V1.Basic.fst +++ b/src/tactics/FStar.Tactics.V1.Basic.fst @@ -261,11 +261,16 @@ let proc_guard' (simplify:bool) (reason:string) (e : env) (g : guard_t) (sc_opt: let! g = goal_of_guard reason e f sc_opt rng in push_goals [g]) - | SMT -> - mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT goal\n" reason (Rel.guard_to_string e g)) (fun () -> + | SMT -> + mlog (fun () -> BU.print2 "Pushing guard (%s:%s) as SMT goal\n" reason (Print.term_to_string f)) (fun () -> let! g = goal_of_guard reason e f sc_opt rng in push_smt_goals [g]) + | SMTSync -> + mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason (Print.term_to_string f)) (fun () -> + Rel.force_trivial_guard e g; + ret ()) + | Force -> mlog (fun () -> BU.print2 "Forcing guard (%s:%s)\n" reason (Rel.guard_to_string e g)) (fun () -> try if not (Env.is_trivial <| Rel.discharge_guard_no_smt e g) diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index a10104b3249..8ae7e4b3aee 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -231,6 +231,45 @@ let with_policy pol (t : tac 'a) : tac 'a = bind (set_guard_policy old_pol) (fun () -> ret r)))) +let proc_guard_formula + (reason:string) (e : env) (f : term) (sc_opt : option should_check_uvar) + (rng:Range.range) +: tac unit += let! ps = get in + match ps.guard_policy with + | Drop -> + // should somehow taint the state instead of just printing a warning + Err.log_issue e.range + (Errors.Warning_TacAdmit, BU.format1 "Tactics admitted guard <%s>\n\n" + (Print.term_to_string f)); + ret () + + | Goal -> + mlog (fun () -> BU.print2 "Making guard (%s:%s) into a goal\n" reason (Print.term_to_string f)) (fun () -> + let! g = goal_of_guard reason e f sc_opt rng in + push_goals [g]) + + | SMT -> + mlog (fun () -> BU.print2 "Pushing guard (%s:%s) as SMT goal\n" reason (Print.term_to_string f)) (fun () -> + let! g = goal_of_guard reason e f sc_opt rng in + push_smt_goals [g]) + + | SMTSync -> + mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason (Print.term_to_string f)) (fun () -> + let g = { Env.trivial_guard with guard_f = NonTrivial f } in + Rel.force_trivial_guard e g; + ret ()) + + | Force -> + mlog (fun () -> BU.print2 "Forcing guard (%s:%s)\n" reason (Print.term_to_string f)) (fun () -> + let g = { Env.trivial_guard with guard_f = NonTrivial f } in + try if not (Env.is_trivial <| Rel.discharge_guard_no_smt e g) + then fail1 "Forcing the guard failed (%s)" reason + else ret () + with + | _ -> mlog (fun () -> BU.print1 "guard = %s\n" (Print.term_to_string f)) (fun () -> + fail1 "Forcing the guard failed (%s)" reason)) + let proc_guard' (simplify:bool) (reason:string) (e : env) (g : guard_t) (sc_opt:option should_check_uvar) (rng:Range.range) : tac unit = mlog (fun () -> BU.print2 "Processing guard (%s:%s)\n" reason (Rel.guard_to_string e g)) (fun () -> @@ -251,35 +290,7 @@ let proc_guard' (simplify:bool) (reason:string) (e : env) (g : guard_t) (sc_opt: match guard_f with | TcComm.Trivial -> ret () | TcComm.NonTrivial f -> - let! ps = get in - match ps.guard_policy with - | Drop -> - // should somehow taint the state instead of just printing a warning - Err.log_issue e.range - (Errors.Warning_TacAdmit, BU.format1 "Tactics admitted guard <%s>\n\n" - (Rel.guard_to_string e g)); - ret () - - | Goal -> - mlog (fun () -> BU.print2 "Making guard (%s:%s) into a goal\n" reason (Rel.guard_to_string e g)) (fun () -> - let! g = goal_of_guard reason e f sc_opt rng in - push_goals [g]) - - | SMT -> - mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT goal\n" reason (Rel.guard_to_string e g)) (fun () -> - let! g = goal_of_guard reason e f sc_opt rng in - push_smt_goals [g]) - - | Force -> - mlog (fun () -> BU.print2 "Forcing guard (%s:%s)\n" reason (Rel.guard_to_string e g)) (fun () -> - try if not (Env.is_trivial <| Rel.discharge_guard_no_smt e g) - then - mlog (fun () -> BU.print1 "guard = %s\n" (Rel.guard_to_string e g)) (fun () -> - fail1 "Forcing the guard failed (%s)" reason) - else ret () - with - | _ -> mlog (fun () -> BU.print1 "guard = %s\n" (Rel.guard_to_string e g)) (fun () -> - fail1 "Forcing the guard failed (%s)" reason))) + proc_guard_formula reason e f sc_opt rng) let proc_guard = proc_guard' true diff --git a/src/tactics/FStar.Tactics.V2.Interpreter.fst b/src/tactics/FStar.Tactics.V2.Interpreter.fst index a0f48944465..27248b61232 100644 --- a/src/tactics/FStar.Tactics.V2.Interpreter.fst +++ b/src/tactics/FStar.Tactics.V2.Interpreter.fst @@ -796,7 +796,8 @@ let run_tactic_on_ps' if !tacdbg then do_dump_proofstate ps "at the finish line"; - (ps.goals@ps.smt_goals, ret) + + (remaining_smt_goals, ret) | Failed (e, ps) -> do_dump_proofstate ps "at the time of failure"; diff --git a/ulib/FStar.Tactics.Types.fsti b/ulib/FStar.Tactics.Types.fsti index bf1e8bae8ff..410d6ab4b00 100644 --- a/ulib/FStar.Tactics.Types.fsti +++ b/ulib/FStar.Tactics.Types.fsti @@ -53,10 +53,11 @@ type ctrl_flag = | Abort type guard_policy = - | SMT - | Goal - | Force - | Drop // unsound! careful! + | Goal // Add guards as (normal) goals + | SMT // Add guards as SMT goals + | SMTSync // Send guards to SMT immediately, will *log* errors (not raise) if anything fails + | Force // Force guards without SMT + | Drop // Drop guards, clearly unsound! careful! type unfold_side = | Left diff --git a/ulib/FStar.Tactics.V1.Builtins.fsti b/ulib/FStar.Tactics.V1.Builtins.fsti index 4439443094c..1e2a0302850 100644 --- a/ulib/FStar.Tactics.V1.Builtins.fsti +++ b/ulib/FStar.Tactics.V1.Builtins.fsti @@ -451,76 +451,3 @@ val t_smt_sync : vconfig -> Tac unit (** This returns the free uvars that appear in a term. This is not a reflection primitive as it depends on the state of the UF graph. *) val free_uvars : term -> Tac (list int) - - -(***** APIs used in the meta DSL framework *****) - -(** Meta DSL framework is an experimental feature - See examples/dsls/ for more details - Following APIs are part of the framework *) - -(** TODO: maybe the equiv APIs should require typing of the arguments? *) - -val check_subtyping (g:env) (t0 t1:typ) - : Tac (option (subtyping_token g t0 t1) & issues) - -val check_equiv (g:env) (t0 t1:typ) - : Tac (option (equiv_token g t0 t1) & issues) - -// -// Compute the type of e using the core typechecker -// -val core_compute_term_type (g:env) (e:term) (eff:tot_or_ghost) - : Tac (option (t:typ{typing_token g e (eff, t)}) & issues) - -// -// Check that e:t using the core typechecker -// -val core_check_term (g:env) (e:term) (t:typ) (eff:tot_or_ghost) - : Tac (option (typing_token g e (eff, t)) & issues) - -// -// Instantiate the implicits in e and compute its type -// -val tc_term (g:env) (e:term) (eff:tot_or_ghost) - : Tac (option (r:(term & typ){typing_token g (fst r) (eff, snd r)}) & issues) - -val universe_of (g:env) (e:term) - : Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Tv_Type u))}) & issues) - -type prop_validity_token (g:env) (t:term) = - e:term{typing_token g t (E_Total, pack_ln (Tv_FVar (pack_fv prop_qn))) /\ - typing_token g e (E_Total, t)} - -val check_prop_validity (g:env) (t:term) - : Tac (option (prop_validity_token g t) & issues) - -// -// Instantiate implicits in t -// -// When the return value is Some (t', ty), -// t' is the elaborated t, and ty is its type -// -// This API does not return a proof for typing of t' -// The client may follow it up with another call to core_check_term get the proof -// -val instantiate_implicits (g:env) (t:term) - : Tac (option (term & typ) & issues) - -val maybe_relate_after_unfolding (g:env) (t1 t2:term) - : Tac (option unfold_side & issues) - -val maybe_unfold_head (g:env) (t0:term) - : Tac (option (t1:term{equiv_token g t0 t1}) & issues) - -val push_open_namespace (g:env) (ns:name) - : Tac env - -val push_module_abbrev (g:env) (n:string) (m:name) - : Tac env - -val resolve_name (g:env) (n:name) - : Tac (option (either bv fv)) - -val log_issues (issues:list FStar.Issue.issue) - : Tac unit