diff --git a/src/ecCoq.ml b/src/ecCoq.ml index 9ef55b691d..a49b1f8342 100644 --- a/src/ecCoq.ml +++ b/src/ecCoq.ml @@ -59,18 +59,11 @@ type w3absmod = { w3am_ty : WTy.ty; } -(* -------------------------------------------------------------------- *) -type kpattern = - | KHole - | KApp of EcPath.path * kpattern list - | KProj of kpattern * int - (* -------------------------------------------------------------------- *) type tenv = { (*---*) te_env : EcEnv.env; mutable te_th : WTheory.theory_uc; (*---*) te_known_w3 : w3_known_op Hp.t; - mutable tk_known_w3 : (kpattern * w3_known_op) list; (*---*) te_ty : w3ty Hp.t; (*---*) te_op : w3op Hp.t; (*---*) te_lc : w3op Hid.t; @@ -89,7 +82,6 @@ let empty_tenv env th ts_mem ts_distr fs_witness fs_mu = { te_env = env; te_th = th; te_known_w3 = Hp.create 0; - tk_known_w3 = []; te_ty = Hp.create 0; te_op = Hp.create 0; te_lc = Hid.create 0; @@ -1250,7 +1242,6 @@ let add_equal_symbole tenv = let init ~env hyps concl = let eenv = LDecl.toenv hyps in - let hyps = LDecl.tohyps hyps in let ts_mem = WTy.create_tysymbol (WIdent.id_fresh "memory") [] WTy.NoDef in let vta = WTy.create_tvsymbol (WIdent.id_fresh "ta") in @@ -1301,11 +1292,15 @@ let init ~env hyps concl = let witness = (fs_witness, witness_theory) in Hp.add known CI_Witness.p_witness witness; + (* lenv must be shared and no fresh generated to ensure we have the same why elements*) + let init_select _ ax = ax.ax_visibility = `Visible in let toadd = EcEnv.Ax.all ~check:init_select eenv in List.iter (trans_axiom tenv) toadd; + let hyps = LDecl.tohyps hyps in let lenv = lenv_of_hyps tenv hyps in + let wterm = Cast.force_prop (trans_form (tenv, lenv) concl) in let pr = WDecl.create_prsymbol (WIdent.id_fresh "goal") in let dec = WDecl.create_prop_decl WDecl.Pgoal pr wterm in @@ -1446,11 +1441,9 @@ let make_output_dir dir = else Unix.mkdir dir 0o770 ; type mode = - | Batch (* Only check scripts *) - | Update (* Check and update scripts *) + | Check (* Check scripts *) | Edit (* Edit then check scripts *) | Fix (* Try to check script, then edit script on non-success *) - | FixUpdate (* Update and fix *) let editor_command pconf config = try @@ -1459,16 +1452,23 @@ let editor_command pconf config = with Not_found -> Why3.Whyconf.(default_editor (get_main config)) -let scriptfile ~(loc:EcLocation.t) ~ext = - let l,r = loc.loc_start in - let sid = string_of_int l ^ string_of_int r in +let scriptfile ~(loc:EcLocation.t) ~name ~ext = let file = loc.loc_fname in let path = Filename.dirname file in let path = path ^ "/.interactive" in make_output_dir path; - let name = Filename.basename file in - let name = Filename.remove_extension name in - Format.sprintf "%s/%s%s%s" path name sid ext + let name = + if String.is_empty name then + begin + let name = Filename.basename file in + let name = Filename.remove_extension name in + let l,r = loc.loc_start in + let sid = string_of_int l ^ string_of_int r in + name ^ sid + end + else name + in + Format.sprintf "%s/%s%s" path name ext let safe_remove f = try Unix.unlink f with Unix.Unix_error _ -> () @@ -1495,56 +1495,35 @@ let editor ~script ~merge ~config pconf driver task = in call_prover_task ~config ~timeout:None ~steps:None pconf.prover call -let prepare ~coqmode ~loc driver task = +let prepare ~name ~loc driver task = let ext = Filename.extension (Why3.Driver.file_of_task driver "S" "T" task) in - let force = coqmode <> Batch in - let script = scriptfile ~loc ~ext in - if Sys.file_exists script then Some (script, true) else - if force then + let script = scriptfile ~loc ~name ~ext in + if Sys.file_exists script then (script, true) else begin pp_to_file script (fun fmt -> ignore @@ Why3.Driver.print_task_prepared driver fmt task ); - Some (script, false) + (script, false) end - else None -let interactive ~notify ~coqmode ~loc pconf ~config driver prover task = +let interactive ~notify ~name ~coqmode ~loc pconf ~config driver prover task = let time = 10 in let timeout = if time <= 0 then None else Some (float time) in - - match prepare ~coqmode ~loc driver task with - | None -> - notify |> oiter (fun notify -> notify `Critical (lazy ( - Format.asprintf "Missing script(s) for prover %a." Why3.Whyconf.print_prover prover - ))); - None - | Some (script, merge) -> - match coqmode with - | Batch -> - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task - | Update -> - if merge then updatescript ~script driver task ; - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task - | Edit -> - editor ~script ~merge ~config pconf driver task |> obind (fun _ -> - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task) - | Fix -> - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task - |> obind (fun r -> - if is_valid r then Some r else - editor ~script ~merge ~config pconf driver task |> obind (fun _ -> - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task)) - | FixUpdate -> - if merge then updatescript ~script driver task ; - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task - |> obind (fun r -> - if is_valid r then Some r else - let merge = false in - editor ~script ~merge ~config pconf driver task - |> obind (fun _ -> - run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task)) + let script, merge = prepare ~name ~loc driver task in + if merge then updatescript ~script driver task ; + match coqmode with + | Check -> + run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task + | Edit -> + editor ~script ~merge ~config pconf driver task |> obind (fun _ -> + run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task) + | Fix -> + run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task + |> obind (fun r -> + if is_valid r then Some r else + editor ~script ~merge ~config pconf driver task |> obind (fun _ -> + run_batch ~script ~timeout ~config pconf driver ~steplimit:None prover task)) let is_trivial (t : Why3.Task.task) = let goal = Why3.Task.task_goal_fmla t in @@ -1556,7 +1535,7 @@ let cfg = lazy (Why3.Whyconf.init_config None) let config () = Lazy.force cfg -let build_proof_task ~notify ~coqmode ~loc ~config ~env task = +let build_proof_task ~notify ~name ~coqmode ~loc ~config ~env task = try let (prover,pconf) = let fp = Why3.Whyconf.parse_filter_prover "Coq" in @@ -1587,7 +1566,7 @@ let build_proof_task ~notify ~coqmode ~loc ~config ~env task = if is_trivial task then Some valid else - interactive ~notify ~coqmode ~loc pconf ~config drv prover task + interactive ~notify ~name ~coqmode ~loc pconf ~config drv prover task with | CoqNotFound -> notify |> oiter (fun notify -> notify `Critical (lazy ( @@ -1600,7 +1579,7 @@ let build_proof_task ~notify ~coqmode ~loc ~config ~env task = ))); None -let check ~loc ?notify ?(coqmode=Fix) (hyps : LDecl.hyps) (concl : form) = +let check ~loc ~name ?notify ?(coqmode=Edit) (hyps : LDecl.hyps) (concl : form) = let config = config () in let main_conf = Why3.Whyconf.get_main config in let ld = Why3.Whyconf.loadpath main_conf in @@ -1610,7 +1589,7 @@ let check ~loc ?notify ?(coqmode=Fix) (hyps : LDecl.hyps) (concl : form) = (* let s = Format.asprintf "%a\n" Why3.Pretty.print_task task in *) (* print_string s; *) - match build_proof_task ~notify ~coqmode ~loc ~config ~env task with + match build_proof_task ~notify ~name ~coqmode ~loc ~config ~env task with | None -> false | Some r -> match r.verdict with | Valid -> true diff --git a/src/ecCoq.mli b/src/ecCoq.mli index 0165bbbc21..1219652fd5 100644 --- a/src/ecCoq.mli +++ b/src/ecCoq.mli @@ -3,11 +3,9 @@ open EcEnv open EcProvers type mode = - | Batch (* Only check scripts *) - | Update (* Check and update scripts *) + | Check (* Check scripts *) | Edit (* Edit then check scripts *) | Fix (* Try to check script, then edit script on non-success *) - | FixUpdate (* Update and fix *) - -val check: loc:EcLocation.t -> ?notify:notify -> ?coqmode:mode-> LDecl.hyps -> form -> bool +val check: loc:EcLocation.t -> name:string -> ?notify:notify -> + ?coqmode:mode-> LDecl.hyps -> form -> bool diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index c1898b2980..f465709c0c 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -149,16 +149,16 @@ let process_smt ?loc (ttenv : ttenv) pi (tc : tcenv1) = (* -------------------------------------------------------------------- *) -let process_coq ~loc (ttenv : ttenv) (pi:EcCoq.mode option) (tc : tcenv1) = +let process_coq ~loc ~name (ttenv : ttenv) (pi:EcCoq.mode option) (tc : tcenv1) = match ttenv.tt_smtmode with | `Admit -> t_admit tc | (`Standard | `Strict) as mode -> - t_seq (t_simplify ~delta:`No) (t_coq ~loc ~mode pi) tc + t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode pi) tc | `Report -> - t_seq (t_simplify ~delta:`No) (t_coq ~loc ~mode:(`Report (Some loc)) pi) tc + t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode:(`Report (Some loc)) pi) tc (* -------------------------------------------------------------------- *) let process_clear symbols tc = diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 511c6d5876..078b275dc8 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -74,7 +74,7 @@ val process_generalize : ?doeq:bool -> genpattern list -> backward val process_move : ?doeq:bool -> ppterm list -> prevert -> backward val process_clear : psymbol list -> backward val process_smt : ?loc:EcLocation.t -> ttenv -> pprover_infos -> backward -val process_coq : loc:EcLocation.t -> ttenv -> EcCoq.mode option -> backward +val process_coq : loc:EcLocation.t -> name:string -> ttenv -> EcCoq.mode option -> backward val process_apply : implicits:bool -> apply_t * prevert option -> backward val process_delta : und_delta:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward val process_rewrite : ttenv -> ?target:psymbol -> rwarg list -> backward diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index efa8608d70..459ae8a101 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -156,7 +156,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) = | Pwlog (ids, b, f) -> process_wlog ~suff:b ids f | Pgenhave gh -> process_genhave ttenv gh | Prwnormal _ -> assert false - | Pcoq pi -> process_coq ~loc:(loc t) ttenv pi + | Pcoq (pi, name) -> process_coq ~loc:(loc t) ~name:name.pl_desc ttenv pi in tx tc diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 28f224b44e..f31fe8d493 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -123,11 +123,9 @@ "assumption" , ASSUMPTION ; (* KW: bytac *) "smt" , SMT ; (* KW: bytac *) "coq" , COQ ; (* KW: bytac *) - "batch" , BATCH ; (* KW: bytac *) - "update" , UPDATE ; (* KW: bytac *) + "check" , CHECK ; (* KW: bytac *) "edit" , EDIT ; (* KW: bytac *) "fix" , FIX ; (* KW: bytac *) - "fixupdate" , FIXUPDATE ; (* KW: bytac *) "by" , BY ; (* KW: bytac *) "reflexivity" , REFLEX ; (* KW: bytac *) "done" , DONE ; (* KW: bytac *) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index d02616f642..8527ecbe32 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2443,7 +2443,7 @@ let t_smt ~(mode:smtmode) pi tc = (* -------------------------------------------------------------------- *) -let t_coq ~loc ~(mode:smtmode) (coqmode:EcCoq.mode option) tc = +let t_coq ~loc ~name ~(mode:smtmode) (coqmode:EcCoq.mode option) tc = let error () = match mode with | `Standard -> @@ -2460,7 +2460,7 @@ let t_coq ~loc ~(mode:smtmode) (coqmode:EcCoq.mode option) tc = let env, hyps, concl = FApi.tc1_eflat tc in let notify = (fun lvl (lazy s) -> EcEnv.notify env lvl "%s" s) in - if EcCoq.check ~loc ~notify ?coqmode hyps concl + if EcCoq.check ~loc ~name ~notify ?coqmode hyps concl then FApi.xmutate1 tc `Smt [] else error () diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index f218562d1b..6515bed356 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -319,7 +319,7 @@ val t_congr : form pair -> form pair list * ty -> FApi.backward type smtmode = [`Standard | `Strict | `Report of EcLocation.t option] val t_smt: mode:smtmode -> prover_infos -> FApi.backward -val t_coq: loc:EcLocation.t -> mode:smtmode -> EcCoq.mode option -> FApi.backward +val t_coq: loc:EcLocation.t -> name:string -> mode:smtmode -> EcCoq.mode option -> FApi.backward (* -------------------------------------------------------------------- *) val t_solve : diff --git a/src/ecParser.mly b/src/ecParser.mly index 3ae10c4281..05c559ffb3 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -421,11 +421,9 @@ %token CONSEQ %token CONST %token COQ -%token BATCH -%token UPDATE +%token CHECK %token EDIT %token FIX -%token FIXUPDATE %token COST %token DEBUG %token DECLARE @@ -2929,8 +2927,8 @@ logtactic: | SMT pi=smt_info { Psmt pi } -| COQ pi=coq_info - { Pcoq pi} +| COQ pi=coq_info name=loc(STRING) + { Pcoq (pi, name)} | SMT LPAREN dbmap=dbmap1* RPAREN { Psmt (SMT.mk_smt_option [`WANTEDLEMMAS dbmap]) } @@ -3868,11 +3866,9 @@ print: coq_info: | { None } -| BATCH { Some EcCoq.Batch } -| UPDATE { Some EcCoq.Update } +| CHECK { Some EcCoq.Check } | EDIT { Some EcCoq.Edit } | FIX { Some EcCoq.Fix } -| FIXUPDATE { Some EcCoq.FixUpdate } smt_info: | li=smt_info1* { SMT.mk_smt_option li} diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 0acd3b8a75..8059cedc27 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -973,7 +973,7 @@ type logtactic = | Pmemory of psymbol | Pgenhave of pgenhave | Pwlog of (psymbol list * bool * pformula) - | Pcoq of EcCoq.mode option + | Pcoq of (EcCoq.mode option * psymbol) (* -------------------------------------------------------------------- *) and ptactic_core_r =