Remove non-strict proof mode.

strub · strub · commit 0df85113c4a3 · 2024-05-16T10:49:52.000+02:00
Non-strict proof-mode allows SMT failures to be catchable
with `try` and affiliated. This tends to lead to hardly
maintainable proofs and is not used anymore.

The commits remove the internal handling of non-strict proof
scripts, removing the `proof strict` / `proof -strict` syntax.

The only leftover is the `try!` tactical that allows to
catch SMT failures. It is useful for debugging purpose but
should not remain in final scripts.
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
@@ -494,8 +494,8 @@ and process_sct_close (scope : EcScope.scope) name =
 and process_tactics (scope : EcScope.scope) t =
   let mode = (Pragma.get ()).pm_check in
   match t with
-  | `Actual t  -> snd (EcScope.Tactics.process scope mode t)
-  | `Proof  pm -> EcScope.Tactics.proof   scope mode pm.pm_strict
+  | `Actual t -> snd (EcScope.Tactics.process scope mode t)
+  | `Proof    -> EcScope.Tactics.proof scope
 
 (* -------------------------------------------------------------------- *)
 and process_save (scope : EcScope.scope) ed =
@@ -524,17 +524,10 @@ and process_proverinfo scope pi =
 
 (* -------------------------------------------------------------------- *)
 and process_pragma (scope : EcScope.scope) opt =
-  let pragma_check mode =
-    match EcScope.goal scope with
-    | Some { EcScope.puc_mode = Some false } ->
-        EcScope.hierror "pragma [Proofs:*] in non-strict proof script";
-    | _ -> pragma_check mode
-  in
-
   match unloc opt with
-  | x when x = Pragmas.Proofs.weak    -> pragma_check   `WeakCheck
-  | x when x = Pragmas.Proofs.check   -> pragma_check   `Check
-  | x when x = Pragmas.Proofs.report  -> pragma_check   `Report
+  | x when x = Pragmas.Proofs.weak    -> pragma_check `WeakCheck
+  | x when x = Pragmas.Proofs.check   -> pragma_check `Check
+  | x when x = Pragmas.Proofs.report  -> pragma_check `Report
 
   | "noop"    -> ()
   | "compact" -> Gc.compact ()
diff --git a/src/ecCommands.mli b/src/ecCommands.mli
@@ -49,7 +49,7 @@ val pp_maybe_current_goal : Format.formatter -> unit
 (* -------------------------------------------------------------------- *)
 val pragma_verbose : bool -> unit
 val pragma_g_prall : bool -> unit
-val pragma_check   : EcScope.Ax.mode -> unit
+val pragma_check   : EcScope.Ax.proofmode -> unit
 
 exception InvalidPragma of string
 
diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
@@ -29,7 +29,7 @@ module LG  = EcCoreLib.CI_Logic
 (* -------------------------------------------------------------------- *)
 type ttenv = {
   tt_provers   : EcParsetree.pprover_infos -> EcProvers.prover_infos;
-  tt_smtmode   : [`Admit | `Strict | `Standard | `Report];
+  tt_smtmode   : [`Admit | `Strict | `Sloppy | `Report];
   tt_implicits : bool;
   tt_oldip     : bool;
   tt_redlogic  : bool;
@@ -141,7 +141,7 @@ let process_smt ?loc (ttenv : ttenv) pi (tc : tcenv1) =
   | `Admit ->
       t_admit tc
 
-  | (`Standard | `Strict) as mode ->
+  | (`Sloppy | `Strict) as mode ->
       t_seq (t_simplify ~delta:`No) (t_smt ~mode pi) tc
 
   | `Report ->
diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli
@@ -10,7 +10,7 @@ open EcProofTerm
 (* -------------------------------------------------------------------- *)
 type ttenv = {
   tt_provers   : EcParsetree.pprover_infos -> EcProvers.prover_infos;
-  tt_smtmode   : [`Admit | `Strict | `Standard | `Report];
+  tt_smtmode   : [`Admit | `Strict | `Sloppy | `Report];
   tt_implicits : bool;
   tt_oldip     : bool;
   tt_redlogic  : bool;
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
@@ -117,7 +117,7 @@ and process1_seq (ttenv : ttenv) (ts : ptactic list) (tc : tcenv1) =
 and process1_nstrict (ttenv : ttenv) (t : ptactic_core) (tc : tcenv1) =
   if ttenv.tt_smtmode <> `Strict then
     tc_error !!tc "try! can only be used in strict proof mode";
-  let ttenv = { ttenv with tt_smtmode = `Standard } in
+  let ttenv = { ttenv with tt_smtmode = `Sloppy } in
   process1_try ttenv t tc
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
@@ -67,7 +67,6 @@
     "first"       , FIRST      ;        (* KW: tactical *)
     "last"        , LAST       ;        (* KW: tactical *)
     "do"          , DO         ;        (* KW: tactical *)
-    "strict"      , STRICT     ;        (* KW: tactical *)
     "expect"      , EXPECT     ;        (* KW: tactical *)
 
     (* Lambda tactics *)
diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
@@ -2411,13 +2411,13 @@ let t_congr (f1, f2) (args, ty) tc =
   doit (List.rev args) ty tc
 
 (* -------------------------------------------------------------------- *)
-type smtmode = [`Standard | `Strict | `Report of EcLocation.t option]
+type smtmode = [`Sloppy | `Strict | `Report of EcLocation.t option]
 
 (* -------------------------------------------------------------------- *)
 let t_smt ~(mode:smtmode) pi tc =
   let error () =
     match mode with
-    | `Standard ->
+    | `Sloppy ->
         tc_error !!tc ~catchable:true  "cannot prove goal"
     | `Strict ->
         tc_error !!tc ~catchable:false "cannot prove goal (strict)"
diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli
@@ -317,7 +317,7 @@ val t_crush_fwd : ?delta:bool -> int -> FApi.backward
 val t_congr : form pair -> form pair list * ty -> FApi.backward
 
 (* -------------------------------------------------------------------- *)
-type smtmode = [`Standard | `Strict | `Report of EcLocation.t option]
+type smtmode = [`Sloppy | `Strict | `Report of EcLocation.t option]
 
 val t_smt: mode:smtmode -> prover_infos -> FApi.backward
 
diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -572,7 +572,6 @@
 %token SPLIT
 %token SPLITWHILE
 %token STAR
-%token STRICT
 %token SUBST
 %token SUFF
 %token SWAP
@@ -664,7 +663,6 @@ _lident:
 | LEFT       { "left"       }
 | RIGHT      { "right"      }
 | SOLVE      { "solve"      }
-| STRICT     { "strict"     }
 | WLOG       { "wlog"       }
 | EXLIM      { "exlim"      }
 | ECALL      { "ecall"      }
@@ -3533,27 +3531,8 @@ toptactic:
 |       t=tactics { t }
 
 tactics_or_prf:
-| t=toptactic  { `Actual t    }
-| p=proof      { `Proof  p    }
-
-proof:
-| PROOF modes=proofmode1* {
-    let seen = Hashtbl.create 0 in
-      List.fold_left
-        (fun pmodes (mode, flag) ->
-           if Hashtbl.mem seen mode then
-             parse_error mode.pl_loc (Some "duplicated flag");
-           Hashtbl.add seen mode ();
-           match unloc mode with
-           | `Strict -> { pmodes with pm_strict = flag; })
-        { pm_strict = true; } modes
-  }
-
-proofmode1:
-| b=boption(MINUS) pm=loc(proofmodename) { (pm, not b) }
-
-proofmodename:
-| STRICT { `Strict }
+| t=toptactic  { `Actual t }
+| PROOF        { `Proof    }
 
 (* -------------------------------------------------------------------- *)
 tcd_toptactic:
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -1260,7 +1260,7 @@ type global_action =
   | GsctOpen     of osymbol_r
   | GsctClose    of osymbol_r
   | Grealize     of prealize located
-  | Gtactics     of [`Proof of proofmode | `Actual of ptactic list]
+  | Gtactics     of [`Proof | `Actual of ptactic list]
   | Gtcdump      of (tcdump * ptactic list)
   | Gprover_info of pprover_infos
   | Gsave        of save located
diff --git a/src/ecScope.ml b/src/ecScope.ml
@@ -291,11 +291,11 @@ type proof_uc = {
 }
 
 and proof_auc = {
-  puc_name   : symbol option;
-  puc_mode   : bool option;
-  puc_jdg    : proof_state;
-  puc_flags  : pucflags;
-  puc_crt    : EcDecl.axiom;
+  puc_name    : symbol option;
+  puc_started : bool;
+  puc_jdg     : proof_state;
+  puc_flags   : pucflags;
+  puc_crt     : EcDecl.axiom;
 }
 
 and proof_ctxt =
@@ -677,39 +677,33 @@ module Tactics = struct
   type prinfos =
     EcCoreGoal.proofenv * (EcCoreGoal.handle * EcCoreGoal.handle list)
 
+  type proofmode = [`WeakCheck | `Check | `Report]
+
   let pi scope pi = Prover.do_prover_info scope pi
 
-  let proof (scope : scope) mode (strict : bool) =
+  let proof (scope : scope) =
     check_state `InActiveProof "proof script" scope;
 
     match (oget scope.sc_pr_uc).puc_active with
     | None -> hierror "no active lemmas"
     | Some (pac, pct) ->
       let pac =
-        match pac.puc_mode with
-        | None when not strict && mode = `WeakCheck -> begin
-            match pac.puc_jdg with
-            | PSNoCheck -> { pac with puc_mode = Some false; }
-            | PSCheck _ ->
-                let pac = { pac with puc_jdg = PSNoCheck } in
-                  { pac with puc_mode = Some false; }
-        end
-
-        | None   -> { pac with puc_mode = Some strict }
-        | Some _ -> hierror "[proof] can only be used at beginning of a proof script"
+        if pac.puc_started then
+          hierror "[proof] can only be used at beginning of a proof script";
+        { pac with puc_started = true }
       in
         { scope with sc_pr_uc =
             Some { (oget scope.sc_pr_uc) with puc_active = Some (pac, pct); } }
 
-  let process_r ?reloc mark mode (scope : scope) (tac : ptactic list) =
+  let process_r ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) =
     check_state `InProof "proof script" scope;
 
     let scope =
       match (oget scope.sc_pr_uc).puc_active with
       | None -> hierror "no active lemma"
       | Some (pac, _) ->
-          if   mark && pac.puc_mode = None
-          then proof scope mode true
+          if   mark && not pac.puc_started
+          then proof scope
           else scope
     in
 
@@ -724,16 +718,10 @@ module Tactics = struct
         let module TTC = EcHiTacticals in
 
         let htmode =
-          match pac.puc_mode, mode with
-          | Some true , `WeakCheck -> `Admit
-          | _         , `WeakCheck ->
-               hierror "cannot weak-check a non-strict proof script"
-          | Some true , `Check     -> `Strict
-          | Some false, `Check     -> `Standard
-          | None      , `Check     -> `Strict
-          | Some true , `Report    -> `Report
-          | Some false, `Report    -> `Standard
-          | None      , `Report    -> `Report
+          match mode with
+          | `WeakCheck -> `Admit
+          | `Check     -> `Strict
+          | `Report    -> `Report
         in
 
         let ttenv = {
@@ -816,7 +804,7 @@ module Ax = struct
 
   module TT = EcTyping
 
-  type mode = [`WeakCheck | `Check | `Report]
+  type proofmode = Tactics.proofmode
 
   (* ------------------------------------------------------------------ *)
   let bind ?(import = EcTheory.import0) (scope : scope) ((x, ax) : _ * axiom) =
@@ -835,19 +823,21 @@ module Ax = struct
           PSCheck proof
     in
     let puc =
-      { puc_active = Some ({
-          puc_name  = name;
-          puc_mode  = None;
-          puc_jdg   = puc;
-          puc_flags = axflags;
-          puc_crt   = axd; }, ctxt);
-        puc_cont = cont;
-        puc_init = scope.sc_env; }
+      let active =        
+        { puc_name    = name
+        ; puc_started = false
+        ; puc_jdg     = puc
+        ; puc_flags   = axflags
+        ; puc_crt     = axd }
+      in
+        { puc_active    = Some (active, ctxt);
+          puc_cont      = cont;
+          puc_init      = scope.sc_env; }
     in
       { scope with sc_pr_uc = Some puc }
 
   (* ------------------------------------------------------------------ *)
-  let rec add_r (scope : scope) (mode : mode) (ax : paxiom located) =
+  let rec add_r (scope : scope) (mode : proofmode) (ax : paxiom located) =
     assert (scope.sc_pr_uc = None);
 
     let env = env scope in
@@ -995,7 +985,7 @@ module Ax = struct
       tintro |> ofold
         (fun t sc -> snd (Tactics.process1_r false `Check sc t))
         scope in
-    let scope = Tactics.proof scope mode (if tc = None then true else false) in
+    let scope = Tactics.proof scope in
 
     let tc =
       match tc with
@@ -1027,11 +1017,11 @@ module Ax = struct
     snd (save_r ~mode:`Abort scope)
 
   (* ------------------------------------------------------------------ *)
-  let add (scope : scope) (mode : mode) (ax : paxiom located) =
+  let add (scope : scope) (mode : proofmode) (ax : paxiom located) =
     add_r scope mode ax
 
   (* ------------------------------------------------------------------ *)
-  let realize (scope : scope) (mode : mode) (rl : prealize located) =
+  let realize (scope : scope) (mode : proofmode) (rl : prealize located) =
     check_state `InProof "activate" scope;
 
     let loc = rl.pl_loc and rl = rl.pl_desc in
@@ -1808,7 +1798,7 @@ module Ty = struct
 
           let escope = scope in
           let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
-          let escope = Tactics.proof escope mode true in
+          let escope = Tactics.proof escope in
           let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
             ignore (Ax.save_r escope))
         axs;
@@ -2298,7 +2288,7 @@ module Cloning = struct
 
           let escope = { scope with sc_env = axc.C.axc_env; } in
           let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
-          let escope = Tactics.proof escope mode true in
+          let escope = Tactics.proof escope in
           let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
             ignore (Ax.save_r escope); None)
       proofs
diff --git a/src/ecScope.mli b/src/ecScope.mli
@@ -36,11 +36,11 @@ type proof_uc = {
 }
 
 and proof_auc = {
-  puc_name   : symbol option;
-  puc_mode   : bool option;
-  puc_jdg    : proof_state;
-  puc_flags  : pucflags;
-  puc_crt    : EcDecl.axiom;
+  puc_name    : symbol option;
+  puc_started : bool;
+  puc_jdg     : proof_state;
+  puc_flags   : pucflags;
+  puc_crt     : EcDecl.axiom;
 }
 
 and proof_ctxt =
@@ -100,21 +100,21 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Ax : sig
-  type mode = [`WeakCheck | `Check | `Report]
+  type proofmode = [`WeakCheck | `Check | `Report]
 
-  val add     : scope -> mode -> paxiom located -> symbol option * scope
+  val add     : scope -> proofmode -> paxiom located -> symbol option * scope
   val save    : scope -> string option * scope
   val admit   : scope -> string option * scope
   val abort   : scope -> scope
-  val realize : scope -> mode -> prealize located -> symbol option * scope
+  val realize : scope -> proofmode -> prealize located -> symbol option * scope
 end
 
 (* -------------------------------------------------------------------- *)
 module Ty : sig
   val add : scope -> ptydecl located -> scope
 
   val add_class    : scope -> ptypeclass located -> scope
-  val add_instance : ?import:EcTheory.import -> scope -> Ax.mode -> ptycinstance located -> scope
+  val add_instance : ?import:EcTheory.import -> scope -> Ax.proofmode -> ptycinstance located -> scope
 end
 
 (* -------------------------------------------------------------------- *)
@@ -178,9 +178,10 @@ module Tactics : sig
   open EcCoreGoal
 
   type prinfos = proofenv * (handle * handle list)
+  type proofmode = Ax.proofmode
 
-  val process : scope -> Ax.mode -> ptactic list -> prinfos option * scope
-  val proof   : scope -> Ax.mode -> bool -> scope
+  val process : scope -> proofmode -> ptactic list -> prinfos option * scope
+  val proof   : scope -> scope
 end
 
 (* -------------------------------------------------------------------- *)
@@ -230,7 +231,7 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Cloning : sig
-  val clone : scope -> Ax.mode -> theory_cloning -> scope
+  val clone : scope -> Ax.proofmode -> theory_cloning -> scope
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/theories/query_counting/OracleBounds.ec b/theories/query_counting/OracleBounds.ec
