diff options
51 files changed, 333 insertions, 207 deletions
diff --git a/.gitattributes b/.gitattributes index 51fa208a7..db179c8d2 100644 --- a/.gitattributes +++ b/.gitattributes @@ -2,10 +2,18 @@ .gitignore export-ignore .mailmap export-ignore -*.out -whitespace +# Because our commit hook automatically does [apply whitespace=fix] we +# disable whitespace checking for all files except those where we want +# it. Otherwise rogue global configuration and forgotten local +# configuration can break commits. +* -whitespace +# tabs are allowed in Makefiles. +Makefile* whitespace=trailing-space +tools/CoqMakefile.in whitespace=trailing-space + +# in general we don't want tabs. *.asciidoc whitespace=trailing-space,tab-in-indent -*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent *.bib whitespace=trailing-space,tab-in-indent *.c whitespace=trailing-space,tab-in-indent *.css whitespace=trailing-space,tab-in-indent @@ -36,3 +44,6 @@ *.v whitespace=trailing-space,tab-in-indent *.xml whitespace=trailing-space,tab-in-indent *.yml whitespace=trailing-space,tab-in-indent + +# CR is desired for these Windows files. +*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent diff --git a/.travis.yml b/.travis.yml index f4f01d2f0..9ec936b0c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -40,10 +40,10 @@ env: # system is == 4.02.3 - COMPILER="system" - COMPILER_BE="4.06.0" - - CAMLP5_VER="6.14" - - CAMLP5_VER_BE="7.03" - - FINDLIB_VER="1.4.1" - - FINDLIB_VER_BE="1.7.3" + - CAMLP5_VER=".6.14" + - CAMLP5_VER_BE=".7.03" + - FINDLIB_VER=".1.4.1" + - FINDLIB_VER_BE=".1.7.3" - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" @@ -76,6 +76,8 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: + # ppx_tools_versioned requires a specific version findlib + - FINDLIB_VER="" - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - if: NOT (type = pull_request) env: @@ -221,7 +223,7 @@ matrix: env: - TEST_TARGET="test-suite" - COMPILER="4.02.3" - - CAMLP5_VER="6.17" + - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-local" before_install: @@ -234,7 +236,7 @@ matrix: env: - TEST_TARGET="" - COMPILER="4.02.3" - - CAMLP5_VER="6.17" + - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error" @@ -264,7 +266,7 @@ install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind.${FINDLIB_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} - opam list script: @@ -54,6 +54,9 @@ Tactics with let bindings in the parameters. - The tactic "dtauto" now handles some inductives such as "@sigT A (fun _ => B)" as non-dependent conjunctions. +- A bug fixed in "rewrite H in *" and "rewrite H in * |-" may cause a + few rare incompatibilities (it was unintendedly recursively + rewriting in the side conditions generated by H). Focusing diff --git a/Makefile.doc b/Makefile.doc index 8cb9c9f0f..3385e4951 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -400,7 +400,7 @@ source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -latex -o $@' - $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ + $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\ $(DOCMLIS) -noheader -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@.tmp $(SHOW)'OCAMLDOC utf8 fix' @@ -410,13 +410,13 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) mli-doc: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \ $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ -css-style style.css ml-dot: $(MLFILES) - $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \ $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot %_dep.png: %.dot @@ -449,7 +449,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(SHOW)'PDFLATEX $*.tex' $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) - $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) + $(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) ########################################################################### # local web server diff --git a/dev/base_include b/dev/base_include index 39e3ef2bd..3320a2a94 100644 --- a/dev/base_include +++ b/dev/base_include @@ -232,7 +232,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc) +let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc) let _ = print_string diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh new file mode 100644 index 000000000..2451657d4 --- /dev/null +++ b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then + ltac2_CI_BRANCH=fix-for/6676 + ltac2_CI_GITURL=https://github.com/gares/ltac2.git + Equations_CI_BRANCH=fix-for/6676 + Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git +fi diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index f819d2e6a..bb7a963aa 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -61,7 +61,7 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Atype u -> print_string "Type(...)" + | Asort u -> print_string "Sort(...)" | Aind(sp,i) -> print_string "Ind("; print_string (MutInd.to_string sp); print_string ","; print_int i; @@ -69,7 +69,6 @@ and ppatom a = and ppwhd whd = match whd with - | Vsort s -> ppsort s | Vprod _ -> print_string "product" | Vfun _ -> print_string "function" | Vfix _ -> print_vfix() diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 1cd23c929..bef31d3fa 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching successively in each of the directories specified in the {\em loadpath}. (see Section~\ref{loadpath}) +Files loaded this way cannot leave proofs open, and neither the {\tt + Load} command can be use inside a proof. + \begin{Variants} \item {\tt Load {\str}.}\label{Load-str}\\ Loads the file denoted by the string {\str}, where {\str} is any @@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em \begin{ErrMsgs} \item \errindex{Can't find file {\ident} on loadpath} +\item \errindex{Load is not supported inside proofs} +\item \errindex{Files processed by Load cannot leave open proofs} \end{ErrMsgs} \section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 66a5f107a..6dca314b4 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal. rewrite H in H2 at - 2}. In particular a failure will happen if any of these three simpler tactics fails. \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in - H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen + H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen as soon as at least one of these simpler tactics succeeds. \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} and \texttt{rewrite H in * |-} that succeeds if at @@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal \item applying the abstracted goal to {\term} \end{enumerate} -For instance, if the current goal $T$ is expressible has $\phi(t)$ +For instance, if the current goal $T$ is expressible as $\phi(t)$ where the notation captures all the instances of $t$ in $\phi(t)$, then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt x}$)$) $t$}. This command can be used, for instance, when the tactic diff --git a/engine/proofview.ml b/engine/proofview.ml index c41b0b0dc..77a884121 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -33,7 +33,7 @@ type entry = (EConstr.constr * EConstr.types) list (* In this version: returns the list of focused goals together with the [evar_map] context. *) let proofview p = - p.comb , p.solution + List.map drop_state p.comb , p.solution let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in @@ -74,7 +74,7 @@ let dependent_init = let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; shelf = [] } + entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } in fun t -> let entry, v = aux t in @@ -110,7 +110,7 @@ let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) (* First component is a reverse list of the goals which come before and second component is the list of the goals which go after (in the expected order). *) -type focus_context = Evar.t list * Evar.t list +type focus_context = goal_with_state list * goal_with_state list (** Returns a stylised view of a focus_context for use by, for @@ -120,7 +120,8 @@ type focus_context = Evar.t list * Evar.t list new nearly identical function everytime. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) -let focus_context f = f +let focus_context (left,right) = + (List.map drop_state left, List.map drop_state right) (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns @@ -149,21 +150,35 @@ let unfocus_sublist (left,right) s = proofview. It returns the focused proofview, and a context for the focus stack. *) let focus i j sp = - let (new_comb, context) = focus_sublist i j sp.comb in - ( { sp with comb = new_comb } , context ) + let (new_comb, (left, right)) = focus_sublist i j sp.comb in + ( { sp with comb = new_comb } , (left, right) ) + +let cleared_alias evd g = + let evk = drop_state g in + let state = get_state g in + Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk) (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). Note that order matters. *) -let undefined defs l = +let undefined_evars defs l = List.fold_right (fun evk l -> match Evarutil.advance defs evk with | Some evk -> List.add_set Evar.equal evk l | None -> l) l [] +let goal_with_state_equal x y = Evar.equal (drop_state x) (drop_state y) +let undefined defs l = + List.fold_right (fun evk l -> + match cleared_alias defs evk with + | Some evk -> List.add_set goal_with_state_equal evk l + | None -> l) l [] (** Unfocuses a proofview with respect to a context. *) -let unfocus c sp = - { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } +let unfocus (left, right) sp = + { sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) } +let with_empty_state = Proofview_monad.with_empty_state +let drop_state = Proofview_monad.drop_state +let goal_with_state = Proofview_monad.goal_with_state (** {6 The tactic monad} *) @@ -406,7 +421,8 @@ let tclFOCUSID id t = try let ev = Evd.evar_key id initial.solution in try - let n = CList.index Evar.equal ev initial.comb in + let comb = CList.map drop_state initial.comb in + let n = CList.index Evar.equal ev comb in (* goal is already under focus *) let (focused,context) = focus n n initial in Pv.set focused >> @@ -415,7 +431,7 @@ let tclFOCUSID id t = return result with Not_found -> (* otherwise, save current focus and work purely on the shelve *) - Comb.set [ev] >> + Comb.set [with_empty_state ev] >> t >>= fun result -> Comb.set initial.comb >> return result @@ -445,7 +461,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -462,7 +478,7 @@ let map_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -488,7 +504,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match Evarutil.advance step goal with + match cleared_alias step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -532,7 +548,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match Evarutil.advance solution goal with + begin match cleared_alias solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -624,12 +640,12 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ initial) + Shelf.modify (fun gls -> gls @ CList.map drop_state initial) let shelve_goals l = let open Proof in Comb.get >>= fun initial -> - let comb = CList.filter (fun g -> not (CList.mem g l)) initial in + let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in Comb.set comb >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >> Shelf.modify (fun gls -> gls @ l) @@ -656,9 +672,27 @@ let free_evars sigma l = in List.map map l +let free_evars_with_state sigma l = + let cache = Evarutil.create_undefined_evars_cache () in + let map ev = + (** Computes the set of evars appearing in the hypotheses, the conclusion or + the body of the evar_info [evi]. Note: since we want to use it on goals, + the body is actually supposed to be empty. *) + let ev = drop_state ev in + let evi = Evd.find sigma ev in + let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in + (ev, fevs) + in + List.map map l + + (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. *) +let unifiable_delayed_with_state sigma g l = + let g = drop_state g in + unifiable_delayed g l + let unifiable sigma g l = let l = free_evars sigma l in unifiable_delayed g l @@ -668,8 +702,8 @@ let unifiable sigma g l = whose definition other goals of [l] depend, and [n] are the non-unifiable goals. *) let partition_unifiable sigma l = - let fevs = free_evars sigma l in - CList.partition (fun g -> unifiable_delayed g fevs) l + let fevs = free_evars_with_state sigma l in + CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -680,7 +714,7 @@ let shelve_unifiable = let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.modify (fun gls -> gls @ u) + Shelf.modify (fun gls -> gls @ CList.map drop_state u) (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -691,13 +725,14 @@ let guard_no_unifiable = match u with | [] -> tclUNIT None | gls -> - let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in + let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in let l = CList.map (fun id -> Names.Name id) l in tclUNIT (Some l) (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) let unshelve l p = + let l = List.map with_empty_state l in (* advance the goals in case of clear *) let l = undefined p.solution l in { p with comb = p.comb@l } @@ -736,7 +771,7 @@ let with_shelf tac = let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in (* Ensure we mark and return only unsolved goals *) - let gls' = undefined sigma (CList.rev_append gls' gls) in + let gls' = undefined_evars sigma (CList.rev_append gls' gls) in let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -818,7 +853,7 @@ let give_up = Comb.set [] >> mark_as_unsafe >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> - Giveup.put initial + Giveup.put (CList.map drop_state initial) @@ -859,8 +894,8 @@ module Progress = struct (** Equality function on goals *) let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in + let evi1 = Evd.find evars1 (drop_state gl1) in + let evi2 = Evd.find evars2 (drop_state gl2) in eq_evar_info evars1 evars2 evi1 evi2 end @@ -1027,10 +1062,12 @@ module Goal = struct env : Environ.env; sigma : Evd.evar_map; concl : EConstr.constr ; + state : StateStore.t; self : Evar.t ; (* for compatibility with old-style definitions *) } let assume (gl : t) = (gl : t) + let state { state=state } = state let env {env} = env let sigma {sigma} = sigma @@ -1038,16 +1075,19 @@ module Goal = struct let concl {concl} = concl let extra {sigma; self} = goal_extra sigma self - let gmake_with info env sigma goal = + let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; concl = EConstr.of_constr (Evd.evar_concl info); + state = state ; self = goal } let nf_gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in let sigma = Evd.add sigma goal info in - gmake_with info env sigma goal , sigma + gmake_with info env sigma goal state , sigma let nf_enter f = InfoL.tag (Info.Dispatch) begin @@ -1063,15 +1103,17 @@ module Goal = struct end end - let normalize { self } = + let normalize { self; state } = Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma self in + let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) let gmake env sigma goal = + let state = get_state goal in + let goal = drop_state goal in let info = Evd.find sigma goal in - gmake_with info env sigma goal + gmake_with info env sigma goal state let enter f = let f gl = InfoL.tag (Info.DBranch) (f gl) in @@ -1104,7 +1146,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match Evarutil.advance sigma goal with + match cleared_alias sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1164,18 +1206,22 @@ module V82 = struct let open Proof in Pv.get >>= fun ps -> try - let tac gl evd = + let tac g_w_s evd = + let g, w = drop_state g_w_s, get_state g_w_s in let glsigma = - tac { Evd.it = gl ; sigma = evd; } in + tac { Evd.it = g ; sigma = evd; } in let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in + let g = CList.map (fun g -> goal_with_state g w) glsigma.Evd.it in ( g, sigma ) in (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution + let (initgoals_w_state, initevd) = + Evd.Monad.List.map (fun g_w_s s -> + let g, w = drop_state g_w_s, get_state g_w_s in + let g, s = goal_nf_evar s g in + goal_with_state g w, s) ps.comb ps.solution in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in + let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> @@ -1190,8 +1236,9 @@ module V82 = struct let nf_evar_goals = Pv.modify begin fun ps -> let map g s = goal_nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { ps with solution = evd; comb = goals; } + let comb = CList.map drop_state ps.comb in + let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in + { ps with solution = evd; } end let has_unresolved_evar pv = @@ -1201,14 +1248,14 @@ module V82 = struct let grab pv = let undef = Evd.undefined_map pv.solution in let goals = CList.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } + { pv with comb = List.map with_empty_state goals } (* Returns the open goals of the proofview together with the evar_map to interpret them. *) let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } + { Evd.it = List.map drop_state comb ; sigma = solution } let top_goals initial { solution=solution; } = let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in @@ -1222,9 +1269,9 @@ module V82 = struct let of_tactic t gls = try - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } + { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in iraise (e, info) diff --git a/engine/proofview.mli b/engine/proofview.mli index 721ce507d..77f30746d 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -72,7 +72,15 @@ val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list val initial_goals : entry -> (constr * types) list +(** goal <-> goal_with_state *) +val with_empty_state : + Proofview_monad.goal -> Proofview_monad.goal_with_state +val drop_state : + Proofview_monad.goal_with_state -> Proofview_monad.goal +val goal_with_state : + Proofview_monad.goal -> Proofview_monad.StateStore.t -> + Proofview_monad.goal_with_state (** {6 Focusing commands} *) @@ -416,14 +424,14 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Evar.t list -> unit tactic + val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Evar.t list -> unit tactic + val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Evar.t list tactic + val tclGETGOALS : Proofview_monad.goal_with_state list tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic @@ -480,6 +488,7 @@ module Goal : sig val env : t -> Environ.env val sigma : t -> Evd.evar_map val extra : t -> Evd.Store.t + val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index d0f471225..494765fc4 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -149,13 +149,25 @@ module Info = struct CList.map_append (collapse_tree n) f end +module StateStore = Store.Make(struct end) + +(* let (set_state, get_state) = StateDyn.Easy.make_dyn "goal_state" *) + +type goal = Evar.t +type goal_with_state = Evar.t * StateStore.t + +let drop_state = fst +let get_state = snd +let goal_with_state g s = (g, s) +let with_empty_state g = (g, StateStore.empty) +let map_goal_with_state f (g, s) = (f g, s) (** Type of proof views: current [evar_map] together with the list of focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Evar.t list; - shelf : Evar.t list; + comb : goal_with_state list; + shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -169,7 +181,7 @@ module P = struct type e = bool (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list + type w = bool * goal list let wunit = true , [] let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 @@ -209,9 +221,9 @@ module Solution : State with type t := Evd.evar_map = struct let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution }) end -module Comb : State with type t = Evar.t list = struct +module Comb : State with type t = goal_with_state list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal_with_state list let get = Logical.map (fun {comb} -> comb) Pv.get let set c = Pv.modify (fun pv -> { pv with comb = c }) let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb }) @@ -227,17 +239,17 @@ module Status : Writer with type t := bool = struct let put s = Logical.put (s, []) end -module Shelf : State with type t = Evar.t list = struct +module Shelf : State with type t = goal list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal list let get = Logical.map (fun {shelf} -> shelf) Pv.get let set c = Pv.modify (fun pv -> { pv with shelf = c }) let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) end -module Giveup : Writer with type t = Evar.t list = struct +module Giveup : Writer with type t = goal list = struct (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list + type t = goal list let put gs = Logical.put (true, gs) end diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index e7123218b..d26816fa6 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -67,12 +67,21 @@ module Info : sig end +module StateStore : Store.S +type goal = Evar.t +type goal_with_state +val drop_state : goal_with_state -> goal +val get_state : goal_with_state -> StateStore.t +val goal_with_state : goal -> StateStore.t -> goal_with_state +val with_empty_state : goal -> goal_with_state +val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state + (** Type of proof views: current [evar_map] together with the list of focused goals. *) type proofview = { solution : Evd.evar_map; - comb : Evar.t list; - shelf : Evar.t list; + comb : goal_with_state list; + shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -81,7 +90,7 @@ module P : sig type s = proofview * Environ.env (** Status (safe/unsafe) * given up *) - type w = bool * Evar.t list + type w = bool * goal list val wunit : w val wprod : w -> w -> w @@ -118,7 +127,7 @@ module Pv : State with type t := proofview module Solution : State with type t := Evd.evar_map (** Lens to the list of focused goals. *) -module Comb : State with type t = Evar.t list +module Comb : State with type t = goal_with_state list (** Lens to the global environment. *) module Env : State with type t := Environ.env @@ -128,11 +137,11 @@ module Status : Writer with type t := bool (** Lens to the list of goals which have been shelved during the execution of the tactic. *) -module Shelf : State with type t = Evar.t list +module Shelf : State with type t = goal list (** Lens to the list of goals which were given up during the execution of the tactic. *) -module Giveup : Writer with type t = Evar.t list +module Giveup : Writer with type t = goal list (** Lens and utilies pertaining to the info trace *) module InfoL : sig diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index aa6c49bc7..586ef1709 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -32,13 +32,12 @@ let cofix_evaluated_tag = 7 let last_variant_tag = 245 type structured_constant = - | Const_sorts of Sorts.t + | Const_sort of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t - | Const_type of Univ.Universe.t type reloc_table = (tag * int) array @@ -46,8 +45,8 @@ type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_sorts _, _ -> false +| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 +| Const_sort _, _ -> false | Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false | Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 @@ -59,13 +58,11 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 -| Const_type _ , _ -> false let rec hash_structured_constant c = let open Hashset.Combine in match c with - | Const_sorts s -> combinesmall 1 (Sorts.hash s) + | Const_sort s -> combinesmall 1 (Sorts.hash s) | Const_ind i -> combinesmall 2 (ind_hash i) | Const_proj p -> combinesmall 3 (Constant.hash p) | Const_b0 t -> combinesmall 4 (Int.hash t) @@ -74,7 +71,6 @@ let rec hash_structured_constant c = let h = Array.fold_left fold 0 a in combinesmall 5 (combine (Int.hash t) h) | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) - | Const_type u -> combinesmall 7 (Univ.Universe.hash u) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -236,20 +232,19 @@ open Util let pp_sort s = let open Sorts in - match family s with - | InSet -> str "Set" - | InProp -> str "Prop" - | InType -> str "Type" + match s with + | Prop Null -> str "Prop" + | Prop Pos -> str "Set" + | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let rec pp_struct_const = function - | Const_sorts s -> pp_sort s + | Const_sort s -> pp_sort s | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) | Const_univ_level l -> Univ.Level.pr l - | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let pp_lbl lbl = str "L" ++ int lbl diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index c8fbb27a9..71dd65186 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -26,13 +26,12 @@ val cofix_evaluated_tag : tag val last_variant_tag : tag type structured_constant = - | Const_sorts of Sorts.t + | Const_sort of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t - | Const_type of Univ.Universe.t val pp_struct_const : structured_constant -> Pp.t diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3104d5751..0d7619e9f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -480,23 +480,23 @@ let rec compile_lam env reloc lam sz cont = (Const_ind ind) (Univ.Instance.to_array u) sz cont | Lsort (Sorts.Prop _ as s) -> - compile_structured_constant reloc (Const_sorts s) sz cont + compile_structured_constant reloc (Const_sort s) sz cont | Lsort (Sorts.Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin + (* We separate global and local universes in [u]. The former will be part + of the structured constant, while the later (if any) will be applied as + arguments. *) + let open Univ in begin let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in if List.is_empty s then - compile_structured_constant reloc (Const_sorts (Sorts.Type u)) sz cont + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont else - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont - in comp_app compile_structured_constant compile_get_univ reloc - (Const_type u) (Array.of_list s) sz cont + (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont end | Llet (id,def,body) -> diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 856b0b465..32d5387b2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -350,7 +350,7 @@ type to_patch = emitcodes * patches * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc + | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index f1e8d1031..5dca69c16 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -833,7 +833,7 @@ let sort_universes g = (** Subtyping of polymorphic contexts *) let check_subtype univs ctxT ctx = - if AUContext.size ctx == AUContext.size ctx then + if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in let push accu v = add_universe v false accu in diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8c7658147..ad9aa4267 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -44,7 +44,6 @@ let rec conv_val env pb k v1 v2 cu = and conv_whd env pb k whd1 whd2 cu = (* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *) match whd1, whd2 with - | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu | Vuniv_level _ , _ | _ , Vuniv_level _ -> (** Both of these are invalid since universes are handled via @@ -81,7 +80,7 @@ and conv_whd env pb k whd1 whd2 cu = (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu - | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ + | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible @@ -119,8 +118,9 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Atype _ , _ | _, Atype _ -> assert false - | Aind _, _ | Aid _, _ -> raise NotConvertible + | Asort s1, Asort s2 -> + sort_cmp_universes env pb s1 s2 cu + | Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env k stk1 stk2 cu = match stk1, stk2 with diff --git a/kernel/vm.ml b/kernel/vm.ml index 352ea74a4..f0bae98dc 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -168,7 +168,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false + | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2d8a1d976..2a784fdf4 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -121,7 +121,7 @@ type vswitch = { type atom = | Aid of Vars.id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (* Zippers *) @@ -136,7 +136,6 @@ type stack = zipper list type to_update = values type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -167,7 +166,6 @@ let uni_lvl_val (v : values) : Univ.Level.t = let pr = let open Pp in match whd with - | Vsort _ -> str "Vsort" | Vprod _ -> str "Vprod" | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" @@ -189,12 +187,17 @@ let rec whd_accu a stk = match Obj.tag at with | i when Int.equal i type_atom_tag -> begin match stk with + | [] -> Vatom_stk(Obj.magic at, stk) | [Zapp args] -> let args = Array.init (nargs args) (arg args) in - let u = Obj.obj (Obj.field at 0) in - let inst = Instance.of_array (Array.map uni_lvl_val args) in - let u = Univ.subst_instance_universe inst u in - Vsort (Type u) + let s = Obj.obj (Obj.field at 0) in + begin match s with + | Type u -> + let inst = Instance.of_array (Array.map uni_lvl_val args) in + let u = Univ.subst_instance_universe inst u in + Vatom_stk (Asort (Type u), []) + | _ -> assert false + end | _ -> assert false end | i when i <= max_atom_tag -> @@ -243,11 +246,8 @@ let whd_val : values -> whd = else let tag = Obj.tag o in if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) + if is_accumulate (fun_code o) then whd_accu o [] + else Vprod(Obj.obj o) else if tag = Obj.closure_tag || tag = Obj.infix_tag then (match kind_of_closure o with @@ -273,7 +273,7 @@ let obj_of_atom : atom -> Obj.t = (* obj_of_str_const : structured_constant -> Obj.t *) let rec obj_of_str_const str = match str with - | Const_sorts s -> Obj.repr (Vsort s) + | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) | Const_proj p -> Obj.repr p | Const_b0 tag -> Obj.repr tag @@ -285,7 +285,6 @@ let rec obj_of_str_const str = done; res | Const_univ_level l -> Obj.repr (Vuniv_level l) - | Const_type u -> obj_of_atom (Atype u) let val_of_obj o = ((Obj.obj o) : values) @@ -502,10 +501,9 @@ let rec pr_atom a = | RelKey i -> str "#" ++ int i | _ -> str "...") ++ str ")" | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") + | Asort _ -> str "Asort(") and pr_whd w = Pp.(match w with - | Vsort _ -> str "Vsort" | Vprod _ -> str "Vprod" | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 350f71372..570e3606a 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -57,7 +57,7 @@ val cofix_upd_code : to_update -> tcode type atom = | Aid of Vars.id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (** Zippers *) @@ -70,7 +70,6 @@ type zipper = type stack = zipper list type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option diff --git a/lib/system.ml b/lib/system.ml index e56736eb1..0ad86c73f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -54,7 +54,8 @@ let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) -let trust_file_cache = ref true +(** Don't trust in interactive mode (the default) *) +let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = diff --git a/parsing/doc.tex b/parsing/doc.tex deleted file mode 100644 index 68ab601cc..000000000 --- a/parsing/doc.tex +++ /dev/null @@ -1,9 +0,0 @@ - -\newpage -\section*{The Coq parsers and printers} - -\ocwsection \label{parsing} -This chapter describes the implementation of the \Coq\ parsers and printers. - -\bigskip -\begin{center}\epsfig{file=parsing.dep.ps}\end{center} diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 794a28dd4..ad6c6df5f 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -239,12 +239,20 @@ END (** Simple induction / destruct *) +let simple_induct h = + Tacticals.New.tclTHEN (Tactics.intros_until h) + (Tacticals.New.onLastHyp Tactics.simplest_elim) + TACTIC EXTEND simple_induction - [ "simple" "induction" quantified_hypothesis(h) ] -> [ Tactics.simple_induct h ] + [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ] END +let simple_destruct h = + Tacticals.New.tclTHEN (Tactics.intros_until h) + (Tacticals.New.onLastHyp Tactics.simplest_case) + TACTIC EXTEND simple_destruct - [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] + [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ] END (** Double induction *) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 6a758ed1f..6c42518b1 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -976,6 +976,7 @@ TACTIC EXTEND unshelve | [ "unshelve" tactic1(t) ] -> [ Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> + let gls = List.map Proofview.with_empty_state gls in Proofview.Unsafe.tclGETGOALS >>= fun ogls -> Proofview.Unsafe.tclSETGOALS (gls @ ogls) ] diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3433987e3..1f2189015 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1568,7 +1568,8 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in let gls = List.rev (Evd.fold_undefined fold undef []) in - match clause, prf with + let gls = List.map Proofview.with_empty_state gls in + match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ Refine.refine ~typecheck:true (fun h -> (h,p)); diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c93b41786..6b7ea2996 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -141,7 +141,6 @@ and nf_vtype env sigma v = nf_val env sigma v crazy_type and nf_whd env sigma whd typ = match whd with - | Vsort s -> mkSort s | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in @@ -182,7 +181,8 @@ and nf_whd env sigma whd typ = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) in nf_univ_args ~nb_univs mk env sigma stk - | Vatom_stk(Atype u, stk) -> assert false + | Vatom_stk(Asort s, stk) -> + assert (List.is_empty stk); mkSort s | Vuniv_level lvl -> assert false diff --git a/proofs/refine.ml b/proofs/refine.ml index 90276951b..73ed70a1a 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -73,6 +73,7 @@ let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in + let state = Proofview.Goal.state gl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -120,6 +121,7 @@ let generic_refine ~typecheck f gl = (** Select the goals *) let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> diff --git a/stm/stm.ml b/stm/stm.ml index e7c371798..fd22a8388 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2949,6 +2949,7 @@ let get_ast ~doc id = match VCS.visit id with | { step = `Cmd { cast = { loc; expr } } } | { step = `Fork (({ loc; expr }, _, _, _), _) } + | { step = `Sideff ((ReplayCommand {loc; expr}) , _) } | { step = `Qed ({ qast = { loc; expr } }, _) } -> Some (Loc.tag ?loc expr) | _ -> None diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index fe163cabc..b8860d3a5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1131,6 +1131,7 @@ module Search = struct let rec result (shelf, ()) i k = foundone := true; Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in let j = List.length gls in (if !typeclasses_debug > 0 then Feedback.msg_debug @@ -1179,7 +1180,7 @@ module Search = struct (if List.is_empty goals then tclUNIT () else let sigma' = mark_unresolvables sigma goals in - with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= + with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>= fun s -> result s i (Some (Option.default 0 k + j))) end in with_shelf res >>= fun (sh, ()) -> @@ -1272,6 +1273,7 @@ module Search = struct search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end in Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in Proofview.tclEVARMAP >>= fun sigma -> let j = List.length gls in (tclDISPATCH (List.init j (fun i -> tac sigma gls i))) diff --git a/tactics/equality.ml b/tactics/equality.ml index 9a1ac768c..32563d9ff 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -533,7 +533,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let rec do_hyps_atleastonce = function | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") | id :: l -> - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) (do_hyps_atleastonce l) in @@ -549,7 +549,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = end in if cl.concl_occs == NoOccurrences then do_hyps else - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) do_hyps diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e7da17cff..0cc0001c1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -408,8 +408,14 @@ module New = struct Proofview.tclIFCATCH t1 (fun () -> tclDISPATCH (Array.to_list a)) (fun _ -> t3) + let tclIFTHENFIRSTELSE t1 t2 t3 = + Proofview.tclIFCATCH t1 + (fun () -> tclEXTEND [t2] (tclUNIT ()) []) + (fun _ -> t3) let tclIFTHENTRYELSEMUST t1 t2 = tclIFTHENELSE t1 (tclTRY t2) t2 + let tclIFTHENFIRSTTRYELSEMUST t1 t2 = + tclIFTHENFIRSTELSE t1 (tclTRY t2) t2 (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index c5d5c8c12..a3bc4707e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -210,6 +210,7 @@ module New : sig val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic + val tclIFTHENFIRSTTRYELSEMUST : unit tactic -> unit tactic -> unit tactic val tclDO : int -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 945b178a1..94622114d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4661,30 +4661,6 @@ let destruct ev clr c l e = induction_gen clr false ev e ((Evd.empty,(c,NoBindings)),(None,l)) None -(* The registered tactic, which calls the default elimination - * if no elimination constant is provided. *) - -(* Induction tactics *) - -(* This was Induction before 6.3 (induction only in quantified premisses) *) -let simple_induct_id s = Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_elim) -let simple_induct_nodep n = Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_elim) - -let simple_induct = function - | NamedHyp id -> simple_induct_id id - | AnonHyp n -> simple_induct_nodep n - -(* Destruction tactics *) - -let simple_destruct_id s = - (Tacticals.New.tclTHEN (intros_until_id s) (Tacticals.New.onLastHyp simplest_case)) -let simple_destruct_nodep n = - (Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp simplest_case)) - -let simple_destruct = function - | NamedHyp id -> simple_destruct_id id - | AnonHyp n -> simple_destruct_nodep n - (* * Eliminations giving the type instead of the proof. * These tactics use the default elimination constant and diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 74415f8d0..100ddf17f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -280,8 +280,6 @@ val simplest_elim : constr -> unit Proofview.tactic val elim : evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic -val simple_induct : quantified_hypothesis -> unit Proofview.tactic - val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> constr with_bindings option -> unit Proofview.tactic @@ -290,7 +288,6 @@ val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern optio val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val simplest_case : constr -> unit Proofview.tactic -val simple_destruct : quantified_hypothesis -> unit Proofview.tactic val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> constr with_bindings option -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 000000000..70f1b3127 --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out new file mode 100644 index 000000000..0904d5540 --- /dev/null +++ b/test-suite/output/Load.out @@ -0,0 +1,6 @@ +f = 2 + : nat +u = I + : True +The command has indeed failed with message: +Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v new file mode 100644 index 000000000..967507415 --- /dev/null +++ b/test-suite/output/Load.v @@ -0,0 +1,7 @@ +Load "output/load/Load_noproof.v". +Print f. + +Load "output/load/Load_proof.v". +Print u. + +Fail Load "output/load/Load_openproof.v". diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v new file mode 100644 index 000000000..aaf1ffe26 --- /dev/null +++ b/test-suite/output/load/Load_noproof.v @@ -0,0 +1 @@ +Definition f := 2. diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v new file mode 100644 index 000000000..204d4ecbf --- /dev/null +++ b/test-suite/output/load/Load_openproof.v @@ -0,0 +1 @@ +Lemma k : True. diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v new file mode 100644 index 000000000..e47f66a19 --- /dev/null +++ b/test-suite/output/load/Load_proof.v @@ -0,0 +1,2 @@ +Lemma u : True. +Proof. exact I. Qed. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 62249666b..448d0082d 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -151,10 +151,25 @@ Abort. (* Check that rewriting within evars still work (was broken in 8.5beta1) *) - Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y. intros; eexists; eexists. rewrite H. Undo. subst. Abort. + +(* Check that iterated rewriting does not rewrite in the side conditions *) +(* Example from Sigurd Schneider, extracted from contrib containers *) + +Lemma EQ + : forall (e e' : nat), True -> e = e'. +Admitted. + +Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1. +Proof. + rewrite <- (EQ v1 v2) in *. + exact v'. + (* There should be only two side conditions *) + exact I. + exact I. +Qed. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5b73471c5..a7065c031 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -153,7 +153,7 @@ let add_compat_require opts v = let set_batch_mode opts = Flags.quiet := true; - System.trust_file_cache := false; + System.trust_file_cache := true; { opts with batch_mode = true } let add_compile opts verbose s = diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index ae0b94476..7ad8e2c05 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -339,6 +339,8 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () +let drop_last_doc = ref None + let rec loop ~time ~state = let open Vernac.State in Sys.catch_break true; @@ -353,7 +355,14 @@ let rec loop ~time ~state = not possible due exceptions. *) in vernac_loop ~state with - | CErrors.Drop -> state + | CErrors.Drop -> + (* Due to using exceptions as a form of control, state here goes + out of sync as [do_vernac] will never return. We must thus do + this hack until we make `Drop` a toplevel-only command. See + bug #6872. *) + let state = { state with sid = Stm.get_current_state ~doc:state.doc } in + drop_last_doc := Some state; + state | CErrors.Quit -> exit 0 | any -> top_stderr (str "Anomaly: main loop exited with exception: " ++ diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 1c1309051..928f3609a 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -35,3 +35,6 @@ val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t (** Main entry point of Coq: read and execute vernac commands. *) val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t + +(** Last document seen after `Drop` *) +val drop_last_doc : Vernac.State.t option ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 26ede1834..deb2c2038 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -34,7 +34,6 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) let coqtop_init_feed = Coqloop.coqloop_feed -let drop_last_doc = ref None (* Default toplevel loop *) let console_toploop_run opts ~state = @@ -44,9 +43,8 @@ let console_toploop_run opts ~state = Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let state = Coqloop.loop ~time:opts.time ~state in + let _ = Coqloop.loop ~time:opts.time ~state in (* Initialise and launch the Ocaml toplevel *) - drop_last_doc := Some state; Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); (* We let the feeder in place for users of Drop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index dedb298e2..510e10dd1 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -15,9 +15,6 @@ val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts val start : unit -> unit -(* Last document seen after `Drop` *) -val drop_last_doc : Vernac.State.t option ref - (* For other toploops *) val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92dee84f3..a84990f91 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -120,16 +120,9 @@ module State = struct end -let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = +let interp_vernac ~time ~check ~interactive ~state (loc,com) = let open State in - let interp v = - match under_control v with - | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in - let fname = CUnix.make_suffix fname ".v" in - let f = Loadpath.locate_file fname in - load_vernac ~time ~verbosely ~check ~interactive ~state f - | _ -> + try (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the document. Hopefully this is fixed when VtMeta can be removed @@ -139,13 +132,17 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = against that... *) let wflags = CWarnings.get_flags () in CWarnings.set_flags "none"; - let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with + let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with | VtProofStep _ | VtMeta | VtStartProof _ -> true | _ -> false in CWarnings.set_flags wflags; - let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in + (* The -time option is only supported from console-based + clients due to the way it prints. *) + if time then print_cmd_header ?loc com; + let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in + let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in (* Main STM interaction *) if ntip <> `NewTip then @@ -165,13 +162,6 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); let new_proof = Proof_global.give_me_the_proof_opt () in { doc = ndoc; sid = nsid; proof = new_proof } - in - try - (* The -time option is only supported from console-based - clients due to the way it prints. *) - if time then print_cmd_header ?loc com; - let com = if time then VernacTime(time, CAst.make ?loc com) else com in - interp com with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) @@ -184,7 +174,7 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac ~time ~verbosely ~check ~interactive ~state file = +let load_vernac ~time ~verbosely ~check ~interactive ~state file = let ft_beautify, close_beautify = if !Flags.beautify_file then let chan_beautify = open_out (file^beautify_suffix) in diff --git a/vernac/classes.ml b/vernac/classes.ml index 93af94ad6..cd5eff4e7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -334,7 +334,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let init_refine = Tacticals.New.tclTHENLIST [ Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); - Proofview.Unsafe.tclNEWGOALS gls; + Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); Tactics.New.reduce_after_refine; ] in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2aee2065c..6b7746db4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1929,6 +1929,8 @@ exception End_of_input without a considerable amount of refactoring. *) let vernac_load interp fname = + if Proof_global.there_are_pending_proofs () then + CErrors.user_err Pp.(str "Load is not supported inside proofs."); let interp x = let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; @@ -1945,8 +1947,13 @@ let vernac_load interp fname = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in - try while true do interp (snd (parse_sentence input)) done - with End_of_input -> () + begin + try while true do interp (snd (parse_sentence input)) done + with End_of_input -> () + end; + (* If Load left a proof open, we fail too. *) + if Proof_global.there_are_pending_proofs () then + CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.") (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands @@ -1957,6 +1964,7 @@ let interp ?proof ~atts ~st c = vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with + (* Loading a file requires access to the control interpreter *) | VernacLoad _ -> assert false (* The STM should handle that, but LOAD bypasses the STM... *) |