diff options
32 files changed, 628 insertions, 371 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8b79dbf810..68bb24ac77 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -697,7 +697,6 @@ library:ci-verdi-raft: library:ci-vst: extends: .ci-template-flambda - allow_failure: true # Plugins are by definition the projects that depend on Coq's ML API diff --git a/azure-pipelines.yml b/azure-pipelines.yml index aba2b05037..98e17e8fe8 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -40,7 +40,7 @@ jobs: - job: macOS pool: - vmImage: 'macOS-10.13' + vmImage: 'macOS-10.14' variables: MACOSX_DEPLOYMENT_TARGET: '10.11' diff --git a/checker/analyze.ml b/checker/analyze.ml index 91137a0ce2..94acba6b05 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -25,6 +25,12 @@ let code_codepointer = 0x10 let code_infixpointer = 0x11 let code_custom = 0x12 let code_block64 = 0x13 +let code_shared64 = 0x14 +let code_string64 = 0x15 +let code_double_array64_big = 0x16 +let code_double_array64_little = 0x17 +let code_custom_len = 0x18 +let code_custom_fixed = 0x19 [@@@ocaml.warning "-37"] type code_descr = @@ -48,8 +54,14 @@ type code_descr = | CODE_INFIXPOINTER | CODE_CUSTOM | CODE_BLOCK64 +| CODE_SHARED64 +| CODE_STRING64 +| CODE_DOUBLE_ARRAY64_BIG +| CODE_DOUBLE_ARRAY64_LITTLE +| CODE_CUSTOM_LEN +| CODE_CUSTOM_FIXED -let code_max = 0x13 +let code_max = 0x19 let magic_number = "\132\149\166\190" @@ -342,7 +354,8 @@ let parse_object chan = let addr = input_int32u chan in for _i = 0 to 15 do ignore (input_byte chan); done; RCode addr - | CODE_CUSTOM -> + | CODE_CUSTOM + | CODE_CUSTOM_FIXED -> begin match input_cstring chan with | "_j" -> Rint64 (input_intL chan) | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false @@ -356,6 +369,11 @@ let parse_object chan = | CODE_DOUBLE_ARRAY8_LITTLE | CODE_DOUBLE_ARRAY32_BIG | CODE_INFIXPOINTER + | CODE_SHARED64 + | CODE_STRING64 + | CODE_DOUBLE_ARRAY64_BIG + | CODE_DOUBLE_ARRAY64_LITTLE + | CODE_CUSTOM_LEN -> Printf.eprintf "Unhandled code %04x\n%!" data; assert false let parse chan = diff --git a/coqpp/dune b/coqpp/dune index 12071c7c05..d4b49301fb 100644 --- a/coqpp/dune +++ b/coqpp/dune @@ -1,9 +1,15 @@ (ocamllex coqpp_lex) (ocamlyacc coqpp_parse) +(library + (name coqpp) + (wrapped false) + (modules coqpp_ast coqpp_lex coqpp_parse coqpp_parser) + (modules_without_implementation coqpp_ast)) + (executable (name coqpp_main) (public_name coqpp) (package coq) - (modules coqpp_ast coqpp_lex coqpp_parse coqpp_parser coqpp_main) - (modules_without_implementation coqpp_ast)) + (libraries coqpp) + (modules coqpp_main)) diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index 3a096fec06..35d0379008 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -24,4 +24,14 @@ mkdir -p _build # Temporary countermeasure to hdiutil error 5341 # head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg" +hdi_opts=(-volname "coq-$VERSION-installer-macos" + -srcfolder "$DMGDIR" + -ov # overwrite existing file + -format UDZO + -imagekey "zlib-level=9" + + # needed for backward compat since macOS 10.14 which uses APFS by default + # see discussion in #11803 + -fs hfs+ + ) +hdiutil create "${hdi_opts[@]}" "_build/coq-$VERSION-installer-macos.dmg" diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 6649820f22..994ff87674 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -105,5 +105,10 @@ images for testing against Coq master. Using these images is highly recommended: - For Docker, see: https://github.com/coq-community/docker-coq + + The https://github.com/coq-community/docker-coq/wiki/CI-setup wiki + page contains additional information and templates to help setting + Docker-based CI up for your Coq project + - For Nix, see the setup at https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 60c266699c..bd7ee46358 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -214,12 +214,16 @@ : "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" ######################################################################## -# Elpi +# Elpi + Hierarchy Builder ######################################################################## : "${elpi_CI_REF:=coq-master}" : "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" : "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" +: "${elpi_hb_CI_REF:=coq-master}" +: "${elpi_hb_CI_GITURL:=https://github.com/math-comp/hierarchy-builder}" +: "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}" + ######################################################################## # fcsl-pcm ######################################################################## diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index d60bf34ba2..4f185db813 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -6,3 +6,7 @@ ci_dir="$(dirname "$0")" git_download elpi ( cd "${CI_BUILD_DIR}/elpi" && make && make install ) + +git_download elpi_hb + +( cd "${CI_BUILD_DIR}/elpi_hb" && make && make install ) diff --git a/doc/changelog/02-specification-language/10858-stuck-classed.md b/doc/changelog/02-specification-language/10858-stuck-classed.md new file mode 100644 index 0000000000..c7186f2c1d --- /dev/null +++ b/doc/changelog/02-specification-language/10858-stuck-classed.md @@ -0,0 +1,12 @@ +- **Changed:** + Typeclass resolution, accessible through :tacn:`typeclasses eauto`, + now suspends constraints according to their modes + instead of failing. If a typeclass constraint does not match + any of the declared modes for its class, the constraint is postponed, and + the proof search continues on other goals. Proof search does a fixed point + computation to try to solve them at a later stage of resolution. It does + not fail if there remain only stuck constraints at the end of resolution. + This makes typeclasses with declared modes more robust with respect to the + order of resolution. + (`#10858 <https://github.com/coq/coq/pull/10858>`_, + fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). @@ -14,7 +14,7 @@ unreleased.rst (env_var SPHINXWARNOPT)) (action - (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index af4e9051bb..7abeca7815 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -385,8 +385,10 @@ few other commands related to typeclasses. .. tacn:: typeclasses eauto :name: typeclasses eauto - This tactic uses a different resolution engine than :tacn:`eauto` and - :tacn:`auto`. The main differences are the following: + This proof search tactic implements the resolution engine that is run + implicitly during type-checking. This tactic uses a different resolution + engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the + following: + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is @@ -422,6 +424,17 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + The mode hints (see :cmd:`Hint Mode`) associated to a class are + taken into account by :tacn:`typeclasses eauto`. When a goal + does not match any of the declared modes for its head (if any), + instead of failing like :tacn:`eauto`, the goal is suspended and + resolution proceeds on the remaining goals. + If after one run of resolution, there remains suspended goals, + resolution is launched against on them, until it reaches a fixed + point when the set of remaining suspended goals does not change. + Using `solve [typeclasses eauto]` can be used to ensure that + no suspended goals remain. + + When considering local hypotheses, we use the union of all the modes declared in the given databases. diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index fc6d0ace0d..8f325f957a 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -1,12 +1,13 @@ # Grammar extraction tool for documentation -`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in -chunks into `.rst` files. The tool currently inserts Sphinx -`productionlist` constructs. It also generates a file with `prodn` constructs -for the entire grammar, but updates to `tacn` and `cmd` constructs must be done -manually since the grammar doesn't have names for them as it does for -nonterminals. There is an option to report which `tacn` and `cmd` were not -found in the `.rst` files. `tacv` and `cmdv` constructs are not processed at all. +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and +inserts it in chunks into `.rst` files. The tool currently inserts +Sphinx `productionlist` and `prodn` constructs (`productionlist` are +gradually being replaced by `prodn` in the manual). Updates to `tacn` +and `cmd` constructs must be done manually since the grammar doesn't +have names for them as it does for nonterminals. There is an option +to report which `tacn` and `cmd` were not found in the `.rst` files. +`tacv` and `cmdv` constructs are not processed at all. The mlg grammars present several challenges to generating an accurate grammar for documentation purposes: diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune new file mode 100644 index 0000000000..3afa21f2cf --- /dev/null +++ b/doc/tools/docgram/dune @@ -0,0 +1,30 @@ +(executable + (name doc_grammar) + (libraries coq.clib coqpp)) + +(env (_ (binaries doc_grammar.exe))) + +(rule + (targets fullGrammar) + (deps + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (glob_files %{project_root}/plugins/ltac/*.mlg) + (glob_files %{project_root}/plugins/micromega/*.mlg) + (glob_files %{project_root}/plugins/nsatz/*.mlg) + (glob_files %{project_root}/plugins/omega/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg)) + (action + (chdir %{project_root} (run doc_grammar -short -no-warn %{deps}))) + (mode promote)) diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 5f61b9a047..7e0360af72 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -37,6 +37,12 @@ let test_pipe_closedcurly = lk_kw "|" >> lk_kw "}" >> check_no_space end +let test_minus_nat = + let open Pcoq.Lookahead in + to_entry "test_minus_nat" begin + lk_kw "-" >> lk_nat >> check_no_space + end + } GRAMMAR EXTEND Gram @@ -122,7 +128,7 @@ GRAMMAR EXTEND Gram ; integer: [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } - | "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ] + | test_minus_nat; "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ] ; natural: [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ] diff --git a/tactics/auto.ml b/tactics/auto.ml index 1dde820075..d68f9271ec 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -303,7 +303,9 @@ let hintmap_of sigma secvars hdc concl = | None -> Hint_db.map_none ~secvars | Some hdc -> if occur_existential sigma concl then - Hint_db.map_existential sigma ~secvars hdc concl + (fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> []) else Hint_db.map_auto sigma ~secvars hdc concl let exists_evaluable_reference env = function @@ -366,11 +368,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = let st = Hint_db.transparent_state db in let flags, l = let l = - match hdc with None -> Hint_db.map_none ~secvars db + match hdc with + | None -> Hint_db.map_none ~secvars db | Some hdc -> if TransparentState.is_empty st then Hint_db.map_auto sigma ~secvars hdc concl db - else Hint_db.map_existential sigma ~secvars hdc concl db + else match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> [] in auto_flags_of_state st, l in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e3f2f18b44..25bd9cc8a8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -309,12 +309,12 @@ let shelve_dependencies gls = let hintmap_of sigma hdc secvars concl = match hdc with - | None -> fun db -> Hint_db.map_none ~secvars db + | None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db) | Some hdc -> fun db -> - if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma ~secvars hdc concl db - else Hint_db.map_existential sigma ~secvars hdc concl db + if Hint_db.use_dn db then (* Using dnet *) + Hint_db.map_eauto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db secvars = @@ -362,15 +362,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm | _ -> AllowAll with e when CErrors.noncritical e -> AllowAll in - let hint_of_db = hintmap_of sigma hdc secvars concl in - let hintl = - List.map_append - (fun db -> - let tacs = hint_of_db db in - let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in - List.map (fun x -> (flags, x)) tacs) - (local_db::db_list) - in let tac_of_hint = fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) -> let tac = function @@ -428,19 +419,40 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm match repr_hint t with | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp)) | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) - in List.map tac_of_hint hintl + in + let hint_of_db = hintmap_of sigma hdc secvars concl in + let hintl = List.map_filter (fun db -> match hint_of_db db with + | ModeMatch l -> Some (db, l) + | ModeMismatch -> None) + (local_db :: db_list) + in + (* In case there is a mode mismatch in all the databases we get stuck. + Otherwise we consider the hints that match. + Recall the local database uses the union of all the modes in the other databases. *) + if List.is_empty hintl then ModeMismatch + else + let hintl = + CList.map_append + (fun (db, tacs) -> + let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in + List.map (fun x -> (flags, x)) tacs) + hintl + in + ModeMatch (List.map tac_of_hint hintl) and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try - e_my_find_search db_list local_db secvars hd true only_classes env sigma concl + (match e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with + | ModeMatch l -> l + | ModeMismatch -> []) with Not_found -> [] let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in try e_my_find_search db_list local_db secvars hd false only_classes env sigma concl - with Not_found -> [] + with Not_found -> ModeMatch [] let cut_of_hints h = List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h @@ -606,6 +618,7 @@ module Search = struct (** In the proof engine failures are represented as exceptions *) exception ReachedLimitEx exception NoApplicableEx + exception StuckClass (** ReachedLimitEx has priority over NoApplicableEx to handle iterative deepening: it should fail when no hints are applicable, @@ -644,8 +657,11 @@ module Search = struct (if backtrack then str" with backtracking" else str" without backtracking")); let secvars = compute_secvars gl in - let poss = - e_possible_resolve hints info.search_hints secvars info.search_only_classes env sigma concl in + match e_possible_resolve hints info.search_hints secvars + info.search_only_classes env sigma concl with + | ModeMismatch -> + Proofview.tclZERO StuckClass + | ModeMatch poss -> (* If no goal depends on the solution of this one or the instances are irrelevant/assumed to be unique, then we don't need to backtrack, as long as no evar appears in the goal @@ -783,6 +799,7 @@ module Search = struct str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx + | (StuckClass,ie) -> Proofview.tclZERO ~info:ie StuckClass | (_,ie) -> Proofview.tclZERO ~info:ie NoApplicableEx in if backtrack then aux (NoApplicableEx,Exninfo.null) poss @@ -841,11 +858,21 @@ module Search = struct begin fun gl -> search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end in + let tac_or_stuck sigma gls i = + Proofview.tclOR + (tac sigma gls i) + (function (StuckClass, _) -> + if !typeclasses_debug > 1 then + Feedback.msg_debug + Pp.(str "Proof search got stuck on a constraint, postponing it."); + Proofview.tclUNIT () + | (e, ie) -> Proofview.tclZERO ~info:ie e) + 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))) + (tclDISPATCH (List.init j (fun i -> tac_or_stuck sigma gls i))) let fix_iterative t = let rec aux depth = @@ -864,7 +891,7 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let eauto_tac mst ?(unique=false) + let eauto_tac_stuck mst ?(unique=false) ~only_classes ?strategy ~depth ~dep hints = let open Proofview in let tac = @@ -902,6 +929,37 @@ module Search = struct Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac else tac in + let rec fixpoint step laststuck = + tac <*> + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclGETGOALS >>= fun stuck -> + begin + if !typeclasses_debug > 0 then + Feedback.msg_debug Pp.(str "Finished run " ++ int step ++ str " of resolution."); + let stuck = List.map Proofview_monad.drop_state stuck in + let stuckset = Evar.Set.of_list stuck in + let () = + if !typeclasses_debug > 1 then + if Evar.Set.cardinal stuckset > 0 then + Feedback.msg_debug Pp.(str "Stuck goals after resolution: " ++ fnl () ++ + Pp.prlist_with_sep spc (fun ev -> Printer.pr_goal {it = ev; sigma}) stuck) + else Feedback.msg_debug Pp.(str "No stuck goals after resolution.") + in + if Evar.Set.is_empty stuckset then tclUNIT () + else if Evar.Set.equal laststuck stuckset then + begin + if !typeclasses_debug > 1 then Feedback.msg_debug Pp.(str "No progress made."); + tclUNIT () + end + else begin + assert(Evar.Set.subset stuckset laststuck); + (* Progress was made *) + if !typeclasses_debug > 1 then + Feedback.msg_debug Pp.(str "Progress made, restarting resolution on stuck goals."); + fixpoint (succ step) stuckset + end + end + in with_shelf numgoals >>= fun (initshelf, i) -> (if !typeclasses_debug > 1 then Feedback.msg_debug (str"Starting resolution with " ++ int i ++ @@ -910,24 +968,28 @@ module Search = struct (if only_classes then str " in only_classes mode" else str " in regular mode") ++ match depth with None -> str ", unbounded" | Some i -> str ", with depth limit " ++ int i)); - tac + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let gls = CList.map Proofview.drop_state gls in + fixpoint 1 (Evar.Set.of_list gls) let eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints = - Hints.wrap_hint_warning @@ eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints + Hints.wrap_hint_warning @@ eauto_tac_stuck mst ?unique ~only_classes ?strategy ~depth ~dep hints let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, nongoals) -> - let goals = + let goalsl = if !typeclasses_dependency_order then top_sort evm goals else Evar.Set.elements goals in + let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>= + fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in let evm = Evd.set_typeclass_evars evm Evar.Set.empty in let fgoals = Evd.save_future_goals evm in let _, pv = Proofview.init evm [] in - let pv = Proofview.unshelve goals pv in + let pv = Proofview.unshelve goalsl pv in try (* Instance may try to call this before a proof is set up! Thus, give_me_the_proof will fail. Beware! *) @@ -938,35 +1000,35 @@ module Search = struct * with | Proof_global.NoCurrentProof -> *) Id.of_string "instance", false in - let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply ~name ~poly env tac pv - in - if not (List.is_empty gaveup) then - CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); - if Proofview.finished pv' then + let finish pv' shelved = let evm' = Proofview.return pv' in - assert(Evd.fold_undefined (fun ev _ acc -> - let okev = Evd.mem evm ev || List.mem ev shelved in - if not okev then - Feedback.msg_debug - (str "leaking evar " ++ int (Evar.repr ev) ++ - spc () ++ pr_ev evm' ev); - acc && okev) evm' true); + assert(Evd.fold_undefined (fun ev _ acc -> + let okev = Evd.mem evm ev || List.mem ev shelved in + if not okev then + Feedback.msg_debug + (str "leaking evar " ++ int (Evar.repr ev) ++ + spc () ++ pr_ev evm' ev); + acc && okev) evm' true); let fgoals = Evd.shelve_on_future_goals shelved fgoals in let evm' = Evd.restore_future_goals evm' fgoals in let nongoals' = Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with | Some ev' -> Evar.Set.add ev acc - | None -> acc) nongoals (Evd.get_typeclass_evars evm') + | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm') in let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in let evm' = Evd.set_typeclass_evars evm' nongoals' in - Some evm' - else raise Not_found + Some evm' + in + let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv in + if not (List.is_empty gaveup) then + CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); + if Proofview.finished pv' then finish pv' shelved + else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found let evars_eauto env evd depth only_classes unique dep mst hints p = - let eauto_tac = eauto_tac mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in + let eauto_tac = eauto_tac_stuck mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in let res = run_on_evars env evd p eauto_tac in match res with | None -> evd @@ -996,7 +1058,11 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full) let modes = List.map Hint_db.modes dbs in let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in - Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs + Proofview.tclIGNORE + (Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs) + (* Stuck goals can remain here, we could shelve them, but this way + the user can use `solve [typeclasses eauto]` to check there are + no stuck goals remaining, or use [typeclasses eauto; shelve] himself. *) (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index dc94e6a6fb..02b24bc145 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -66,4 +66,6 @@ module Search : sig -> Hints.hint_db list (** The list of hint databases to use *) -> unit Proofview.tactic + (** Note: there might be stuck goals due to mode declarations + remaining even in case of success of the tactic. *) end diff --git a/tactics/eauto.ml b/tactics/eauto.ml index aca6b4734a..9715661985 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -124,7 +124,10 @@ let hintmap_of sigma secvars hdc concl = | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> if occur_existential sigma concl then - (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db) + (fun db -> + match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> []) else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 731792e34e..e9ed43e3de 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -499,6 +499,10 @@ let rec subst_hints_path subst hp = type hint_db_name = string +type 'a with_mode = + | ModeMatch of 'a + | ModeMismatch + module Hint_db : sig type t @@ -507,9 +511,9 @@ val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode val map_eauto : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode val map_auto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t @@ -528,7 +532,6 @@ val add_modes : hint_mode array list GlobRef.Map.t -> t -> t val modes : t -> hint_mode array list GlobRef.Map.t val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a - end = struct @@ -618,8 +621,8 @@ struct let map_existential sigma ~secvars (k,args) concl db = let se = find k db in if matches_modes sigma args se.sentry_mode then - merge_entry secvars db se.sentry_nopat se.sentry_pat - else merge_entry secvars db [] [] + ModeMatch (merge_entry secvars db se.sentry_nopat se.sentry_pat) + else ModeMismatch (* [c] contains an existential *) let map_eauto sigma ~secvars (k,args) concl db = @@ -627,8 +630,8 @@ struct if matches_modes sigma args se.sentry_mode then let st = if db.use_dn then Some db.hintdb_state else None in let pat = lookup_tacs sigma concl st se in - merge_entry secvars db [] pat - else merge_entry secvars db [] [] + ModeMatch (merge_entry secvars db [] pat) + else ModeMismatch let is_exact = function | Give_exact _ -> true @@ -1519,7 +1522,9 @@ let pr_hint_term env sigma cl = let fn = try let hdc = decompose_app_bound sigma cl in if occur_existential sigma cl then - Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl + (fun db -> match Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl db with + | ModeMatch l -> l + | ModeMismatch -> []) else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl with Bound -> Hint_db.map_none ~secvars:Id.Pred.full in diff --git a/tactics/hints.mli b/tactics/hints.mli index 7bb17489bf..2663f65851 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -125,6 +125,10 @@ val glob_hints_path_atom : val glob_hints_path : Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen +type 'a with_mode = + | ModeMatch of 'a + | ModeMismatch + module Hint_db : sig type t @@ -140,16 +144,20 @@ module Hint_db : val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the - arguments, _not_ using the discrimination net. *) + arguments, _not_ using the discrimination net. + Returns a [ModeMismatch] if there are declared modes and none matches. + *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (GlobRef.t * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode (** All hints associated to the reference, respecting modes if evars appear in the - arguments and using the discrimination net. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list + arguments and using the discrimination net. + Returns a [ModeMismatch] if there are declared modes and none matches. *) + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode - (** All hints associated to the reference, respecting modes if evars appear in the - arguments. *) + (** All hints associated to the reference. + Precondition: no evars should appear in the arguments, so no modes + are checked. *) val map_auto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list diff --git a/test-suite/bugs/closed/bug_9058.v b/test-suite/bugs/closed/bug_9058.v new file mode 100644 index 0000000000..6de8324641 --- /dev/null +++ b/test-suite/bugs/closed/bug_9058.v @@ -0,0 +1,16 @@ +Class A (X : Type) := {}. +Hint Mode A ! : typeclass_instances. + +Class B X {aX: A X} Y := { opB: X -> Y -> Y }. +Hint Mode B - - ! : typeclass_instances. + +Section Section. + +Context X {aX: A X} Y {bY: B X Y}. + +(* Set Typeclasses Debug. *) + +Let ok := fun (x : X) (y : Y) => opB x y. +Let ok' := fun x (y : Y) => opB x y. + +End Section. diff --git a/test-suite/success/HintMode.v b/test-suite/success/HintMode.v new file mode 100644 index 0000000000..decddb73d1 --- /dev/null +++ b/test-suite/success/HintMode.v @@ -0,0 +1,20 @@ +Module Postponing. + +Class In A T := { IsIn : A -> T -> Prop }. +Class Empty T := { empty : T }. +Class EmptyIn (A T : Type) `{In A T} `{Empty T} := + { isempty : forall x, IsIn x empty -> False }. + +Hint Mode EmptyIn ! ! - - : typeclass_instances. +Hint Mode Empty ! : typeclass_instances. +Hint Mode In ! - : typeclass_instances. +Existing Class IsIn. +Goal forall A T `{In A T} `{Empty T} `{EmptyIn A T}, forall x : A, IsIn x empty -> False. + Proof. + intros. + eapply @isempty. (* Second goal needs to be solved first, to un-stuck the first one + (hence the Existing Class IsIn to allow finding the assumption of IsIn here) *) + all:typeclasses eauto. +Qed. + +End Postponing. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3f96bf2c35..66305dfefa 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,64 @@ +Module applydestruct. + Class Foo (A : Type) := + { bar : nat -> A; + baz : A -> nat }. + Hint Mode Foo + : typeclass_instances. + + Class C (A : Type). + Hint Mode C + : typeclass_instances. + + Variable fool : forall {A} {F : Foo A} (x : A), C A -> bar 0 = x. + (* apply leaves non-dependent subgoals of typeclass type + alone *) + Goal forall {A} {F : Foo A} (x : A), bar 0 = x. + Proof. + intros. apply fool. + match goal with + |[ |- C A ] => idtac + end. + Abort. + + Variable fooli : forall {A} {F : Foo A} {c : C A} (x : A), bar 0 = x. + (* apply tries to resolve implicit argument typeclass + constraints. *) + Goal forall {A} {F : Foo A} (x : A), bar 0 = x. + Proof. + intros. + Fail apply fooli. + Fail unshelve eapply fooli; solve [typeclasses eauto]. + eapply fooli. + Abort. + + (* It applies resolution after unification of the goal *) + Goal forall {A} {F : Foo A} {C : C A} (x : A), bar 0 = x. + Proof. + intros. apply fooli. + Abort. + Set Typeclasses Debug Verbosity 2. + + Inductive bazdestr {A} (F : Foo A) : nat -> Prop := + | isbas : bazdestr F 1. + + Variable fooinv : forall {A} {F : Foo A} (x : A), + bazdestr F (baz x). + + (* Destruct applies resolution early, before finding + occurrences to abstract. *) + Goal forall {A} {F : Foo A} {C : C A} (x : A), baz x = 0. + Proof. + intros. Fail destruct (fooinv _). + destruct (fooinv x). + Abort. + + Goal forall {A} {F : Foo A} (x y : A), x = y. + Proof. + intros. rewrite <- (fool x). rewrite <- (fool y). reflexivity. + match goal with + |[ |- C A ] => idtac + end. + Abort. +End applydestruct. + Module onlyclasses. (* In 8.6 we still allow non-class subgoals *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index d97bf6724c..2e9f0283ca 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -277,18 +277,3 @@ let context ~poly l = if Global.sections_are_opened () then context_insection sigma ~poly ctx else context_nosection sigma ~poly ctx - -(* Deprecated *) -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name = -let open DeclareDef in -match scope with -| Discharge -> - let univs = match univs with - | Monomorphic_entry univs -> univs - | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs - in - let () = Declare.declare_universe_context ~poly univs in - declare_variable is_coe ~kind typ imps impl name; - GlobRef.VarRef name.CAst.v, Univ.Instance.empty -| Global local -> - declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index ae9edefcac..f5192fc696 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -50,19 +50,3 @@ val context : poly:bool -> local_binder_expr list -> unit - -(** Deprecated *) -val declare_assumption - : coercion_flag - -> poly:bool - -> scope:DeclareDef.locality - -> kind:Decls.assumption_object_kind - -> Constr.types - -> Entries.universes_entry - -> UnivNames.universe_binders - -> Impargs.manual_implicits - -> Glob_term.binding_kind - -> Declaremods.inline - -> variable CAst.t - -> GlobRef.t * Univ.Instance.t -[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."] diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index b6843eab33..65dffb3c0b 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,8 +255,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs | None -> Decls.CoFixpoint, true, [] in let thms = - List.map3 (fun name t (ctx,impargs,_) -> - { Lemmas.Recthm.name; typ = EConstr.of_constr t + List.map3 (fun name typ (ctx,impargs,_) -> + { Lemmas.Recthm.name; typ ; args = List.map RelDecl.get_name ctx; impargs}) fixnames fixtypes fiximps in let init_tac = @@ -272,8 +272,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Decls.Fixpoint - | None -> [], true, Decls.CoFixpoint + | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint) + | None -> [], true, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -294,11 +294,13 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in - let fixdecls = List.map mk_pure fixdecls in - ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx) - fixnames fixdecls fixtypes fiximps); + let udecl = Evd.universe_binders evd in + let _ : GlobRef.t list = + List.map4 (fun name body types imps -> + let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in + DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps) + fixnames fixdecls fixtypes fiximps + in recursive_message (not cofix) gidx fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2b6f987fa6..39fd332184 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -45,32 +45,51 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let fix_exn = Declare.Internal.get_fix_exn ce in - let gr = match scope with + let should_suggest = ce.Declare.proof_entry_opaque && + Option.is_empty ce.Declare.proof_entry_secctx in + let dref = match scope with | Discharge -> - let () = - declare_variable ~name ~kind (SectionLocalDef ce) - in - Names.GlobRef.VarRef name + let () = declare_variable ~name ~kind (SectionLocalDef ce) in + if should_suggest then Proof_using.suggest_variable (Global.env ()) name; + Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in - let gr = Names.GlobRef.ConstRef kn in - let () = DeclareUniv.declare_univ_binders gr udecl in - gr + let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in + let gr = Names.GlobRef.ConstRef kn in + if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; + let () = DeclareUniv.declare_univ_binders gr udecl in + gr in - let () = maybe_declare_manual_implicits false gr imps in + let () = maybe_declare_manual_implicits false dref imps in let () = definition_message name in begin match hook_data with | None -> () | Some (hook, uctx, obls) -> - Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref = gr } + Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref } end; - gr + dref -let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - let kind = Decls.IsDefinition kind in - declare_definition ~name ~scope ~kind ?hook_data udecl ce imps +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + let local = match scope with + | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified + | Global local -> local + in + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry pe in + let kn = Declare.declare_constant ~name ~local ~kind decl in + let dref = Names.GlobRef.ConstRef kn in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Declare.assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in + let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in + dref + +(* Preparing proof entries *) let check_definition_evars ~allow_evars sigma = let env = Global.env () in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1bb6620886..c668ab2ac4 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -49,17 +49,14 @@ val declare_definition -> Impargs.manual_implicits -> GlobRef.t -val declare_fix - : ?opaque:bool - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) +val declare_assumption + : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> name:Id.t -> scope:locality - -> kind:Decls.definition_object_kind - -> UnivNames.universe_binders - -> Entries.universes_entry - -> Evd.side_effects Entries.proof_output - -> Constr.types - -> Impargs.manual_implicits + -> hook:Hook.t option + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Entries.parameter_entry -> GlobRef.t val prepare_definition diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index dcb28b898f..eb9b896ec6 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -376,9 +376,6 @@ let compute_possible_guardness_evidences n fixbody fixtype = let ctx = fst (Term.decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = - ((c, Univ.ContextSet.empty), Evd.empty_side_effects) - let declare_mutual_definition l = let len = List.length l in let first = List.hd l in @@ -410,7 +407,6 @@ let declare_mutual_definition l = let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in let fixnames = first.prg_deps in let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> @@ -421,20 +417,23 @@ let declare_mutual_definition l = Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in ( Some indexes - , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l + , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l ) | IsCoFixpoint -> - (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) + (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l) in (* Declare the recursive definitions *) let poly = first.prg_poly in let scope = first.prg_scope in let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in + let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in + let udecl = UnivNames.empty_binders in let kns = List.map4 - (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind - UnivNames.empty_binders univs) + (fun name body types imps -> + let ce = Declare.definition_entry ~opaque ~types ~univs body in + DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps) fixnames fixdecls fixtypes fiximps in (* Declare notations *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 68f4f55d0e..231bdafce9 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -11,15 +11,8 @@ (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) -open CErrors open Util -open Pp open Names -open Constr -open Declareops -open Nameops -open Pretyping -open Impargs module NamedDecl = Context.Named.Declaration @@ -49,7 +42,7 @@ end module Recthm = struct type t = { name : Id.t - ; typ : EConstr.t + ; typ : Constr.t ; args : Name.t list ; impargs : Impargs.manual_implicits } @@ -136,7 +129,7 @@ let start_dependent_lemma ~name ~poly let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun { Recthm.name; typ } -> name,typ) thms with + match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -144,7 +137,7 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with + in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false @@ -164,7 +157,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua let () = match thms with [_] -> () | _ -> assert false in Some (intro_tac (List.hd thms)), [] in match thms with - | [] -> anomaly (Pp.str "No proof to start.") + | [] -> CErrors.anomaly (Pp.str "No proof to start.") | { Recthm.name; typ; impargs; _}::other_thms -> let info = Info.{ hook @@ -175,7 +168,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua ; scope ; kind } in - let lemma = start_lemma ~name ~poly ~udecl ~info sigma typ in + let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Proof_global.map_proof (fun p -> match init_tac with | None -> p @@ -185,132 +178,167 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua (* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) -(* Helper for process_recthms *) -let retrieve_first_recthm uctx = function - | GlobRef.VarRef id -> - NamedDecl.get_value (Global.lookup_named id), - Decls.variable_opacity id - | GlobRef.ConstRef cst -> - let cb = Global.lookup_constant cst in - (* we get the right order somehow but surely it could be enforced in a better way *) - let uctx = UState.context uctx in - let inst = Univ.UContext.instance uctx in - let map (c, _, _) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) - | _ -> assert false - -(* Helper for process_recthms *) -let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Recthm.name; typ; impargs } = - let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in - let body = Option.map EConstr.of_constr body in - let univs = UState.check_univ_decl ~poly uctx udecl in - let t_i = norm typ in - let kind = Decls.(IsAssumption Conjectural) in - match body with - | None -> - let open DeclareDef in - (match scope with - | Discharge -> - (* Let Fixpoint + Admitted gets turned into axiom so scope is Global, - see finish_admitted *) - assert false - | Global local -> - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry (None,(t_i,univs),None) in - let kn = Declare.declare_constant ~name ~local ~kind decl in - GlobRef.ConstRef kn, impargs) - | Some body -> - let body = norm body in - let rec body_i t = match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) - | App (t, args) -> mkApp (body_i t, args) - | _ -> - anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in - let body_i = body_i body in - let open DeclareDef in - match scope with - | Discharge -> - let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - GlobRef.VarRef name, impargs - | Global local -> - let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in - let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - GlobRef.ConstRef kn, impargs - -(* This declares implicits and calls the hooks for all the theorems, - including the main one *) -let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms = - let other_thms_data = - if List.is_empty other_thms then [] else - (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm uctx dref in - List.map_i (save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq) 1 other_thms in - let thms_data = (dref,imps)::other_thms_data in - List.iter (fun (dref,imps) -> - maybe_declare_manual_implicits false dref imps; - DeclareDef.Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref})) thms_data +(* Support for mutually proved theorems *) + +(* XXX: Most of this does belong to Declare, due to proof_entry manip *) +module MutualEntry : sig + + (* We keep this type abstract and to avoid uncontrolled hacks *) + type t + + val variable : info:Info.t -> Entries.parameter_entry -> t + + val adjust_guardness_conditions + : info:Info.t + -> Evd.side_effects Declare.proof_entry + -> t + + val declare_mutdef + (* Common to all recthms *) + : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> poly:bool + -> uctx:UState.t + -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list + -> udecl:UState.universe_decl + (* Only for the first constant, introduced by compat *) + -> ubind:UnivNames.universe_binders + -> name:Id.t + -> t + -> Names.GlobRef.t list + +end = struct + + (* Body with the fix *) + type et = + | NoBody of Entries.parameter_entry + | Single of Evd.side_effects Declare.proof_entry + | Mutual of Evd.side_effects Declare.proof_entry + + type t = + { entry : et + ; info : Info.t + } + + let variable ~info t = { entry = NoBody t; info } + + (* XXX: Refactor this with the code in + [ComFixpoint.declare_fixpoint_generic] *) + let guess_decreasing env possible_indexes ((body, ctx), eff) = + let open Constr in + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = Pretyping.search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff + + let adjust_guardness_conditions ~info const = + let entry = match info.Info.compute_guard with + | [] -> + (* Not a recursive statement *) + Single const + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + let pe = Declare.Internal.map_entry_body const + ~f:(guess_decreasing env possible_indexes) + in + Mutual pe + in { entry; info } + + let rec select_body i t = + let open Constr in + match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t) + | App (t, args) -> mkApp (select_body i t, args) + | _ -> + CErrors.anomaly + Pp.(str "Not a proof by induction: " ++ + Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") + + let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name ?typ ~impargs ~info mutpe i = + let { Info.hook; compute_guard; scope; kind; _ } = info in + match mutpe with + | NoBody pe -> + DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe + | Single pe -> + (* We'd like to do [assert (i = 0)] here, however this codepath + is used when declaring mutual cofixpoints *) + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs + | Mutual pe -> + (* if typ = None , we don't touch the type; used in the base case *) + let pe = + match typ with + | None -> pe + | Some typ -> + Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) + in + let pe = Declare.Internal.map_entry_body pe + ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs + + let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name { entry; info } = + (* At some point make this a single iteration *) + (* impargs here are special too, fixed in upcoming PRs *) + let impargs = info.Info.impargs in + let r = declare_mutdef ?fix_exn ~poly ~info ~udecl ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in + (* Before we used to do this, check if that's right *) + let ubind = UnivNames.empty_binders in + let rs = + List.map_i ( + fun i { Recthm.name; typ; impargs } -> + declare_mutdef ?fix_exn ~poly ~udecl ~info ~ubind ?hook_data ~uctx ~name ~typ ~impargs entry i) 1 info.Info.other_thms + in r :: rs +end (************************************************************************) (* Admitting a lemma-like constant *) (************************************************************************) (* Admitted *) -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ - spc () ++ strbrk "declared as an axiom.") - let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref ~depr:false ~key:["Keep"; "Admitted"; "Variables"] ~value:true -let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs other_thms = - let open DeclareDef in - let local = match scope with - | Global local -> local - | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified - in - let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in - let () = Declare.assumption_message name in - DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); - (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms +let compute_proof_using_for_admitted proof typ pproofs = + if not (get_keep_admitted_vars ()) then None + else match Proof_global.get_used_variables proof, pproofs with + | Some _ as x, _ -> x + | None, pproof :: _ -> + let env = Global.env () in + let ids_typ = Environ.global_vars_set env typ in + (* [pproof] is evar-normalized by [partial_proof]. We don't + count variables appearing only in the type of evars. *) + let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) + | _ -> None + +let finish_admitted ~name ~poly ~info ~uctx ~udecl pe = + let mutpe = MutualEntry.variable ~info pe in + let ubind = UnivNames.empty_binders in + let _r : Names.GlobRef.t list = + MutualEntry.declare_mutdef ~uctx ~poly ~udecl ~ubind ~name mutpe in + () let save_lemma_admitted ~(lemma : t) : unit = - (* Used for printing in recthms *) - let env = Global.env () in - let { Info.hook; scope; impargs; other_thms } = lemma.info in let udecl = Proof_global.get_universe_decl lemma.proof in - let Proof.{ sigma; name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in + let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ - | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") + | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") in let typ = EConstr.Unsafe.to_constr typ in let proof = Proof_global.get_proof lemma.proof in let pproofs = Proof.partial_proof proof in - let sec_vars = - if not (get_keep_admitted_vars ()) then None - else match Proof_global.get_used_variables lemma.proof, pproofs with - | Some _ as x, _ -> x - | None, pproof :: _ -> - let env = Global.env () in - let ids_typ = Environ.global_vars_set env typ in - (* [pproof] is evar-normalized by [partial_proof]. We don't - count variables appearing only in the type of evars. *) - let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in - Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) - | _ -> None in + let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms + finish_admitted ~name ~poly ~info:lemma.info ~uctx:universes ~udecl (sec_vars, (typ, ctx), None) (************************************************************************) (* Saving a lemma-like constant *) @@ -319,29 +347,12 @@ let save_lemma_admitted ~(lemma : t) : unit = let default_thm_id = Id.of_string "Unnamed_thm" let check_anonymity id save_ident = - if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - user_err Pp.(str "This command can only be used for unnamed theorem.") - -(* Support for mutually proved theorems *) + if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then + CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.") -(* Helper for finish_proved *) -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - Declare.Internal.map_entry_body const - ~f:(fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) - -let finish_proved env sigma idopt po info = +let finish_proved idopt po info = let open Proof_global in - let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in + let { Info.hook } = info in match po with | { name; entries=[const]; universes; udecl; poly } -> let name = match idopt with @@ -349,37 +360,18 @@ let finish_proved env sigma idopt po info = | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in let fix_exn = Declare.Internal.get_fix_exn const in let () = try - let const = adjust_guardness_conditions const compute_guard in - let should_suggest = const.Declare.proof_entry_opaque && - Option.is_empty const.Declare.proof_entry_secctx in - let open DeclareDef in - let r = match scope with - | Discharge -> - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - let () = if should_suggest - then Proof_using.suggest_variable (Global.env ()) name - in - GlobRef.VarRef name - | Global local -> - let kn = - Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - let () = if should_suggest - then Proof_using.suggest_constant (Global.env ()) kn - in - let gr = GlobRef.ConstRef kn in - DeclareUniv.declare_univ_binders gr (UState.universe_binders universes); - gr - in - Declare.definition_message name; - (* This takes care of the implicits and hook for the current constant*) - process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms + let mutpe = MutualEntry.adjust_guardness_conditions ~info const in + let hook_data = Option.map (fun hook -> hook, universes, []) hook in + let ubind = UState.universe_binders universes in + let _r : Names.GlobRef.t list = + MutualEntry.declare_mutdef ~fix_exn ~uctx:universes ~poly ~udecl ?hook_data ~ubind ~name mutpe + in () with e when CErrors.noncritical e -> let e = Exninfo.capture e in Exninfo.iraise (fix_exn e) in () | _ -> - CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") + CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") let finish_derived ~f ~name ~idopt ~entries = (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) @@ -399,7 +391,7 @@ let finish_derived ~f ~name ~idopt ~entries = let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in - let f_kn_term = mkConst f_kn in + let f_kn_term = Constr.mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by references to the constant [f] declared above. This substitution @@ -427,7 +419,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = let id = match Evd.evar_ident ev sigma0 with | Some id -> id - | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) + | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) in let entry, args = Declare.Internal.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in @@ -438,12 +430,12 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = in hook recobls sigma -let finalize_proof idopt env sigma proof_obj proof_info = +let finalize_proof idopt proof_obj proof_info = let open Proof_global in let open Proof_ending in match CEphemeron.default proof_info.Info.proof_ending Regular with | Regular -> - finish_proved env sigma idopt proof_obj proof_info + finish_proved idopt proof_obj proof_info | End_obligation oinfo -> DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo | End_derive { f ; name } -> @@ -453,35 +445,26 @@ let finalize_proof idopt env sigma proof_obj proof_info = let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) - let env = Global.env () in - let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in - finalize_proof idopt env sigma proof_obj lemma.info + finalize_proof idopt proof_obj lemma.info (***********************************************************************) (* Special case to close a lemma without forcing a proof *) (***********************************************************************) let save_lemma_admitted_delayed ~proof ~info = let open Proof_global in - let env = Global.env () in - let sigma = Evd.from_env env in let { name; entries; universes; udecl; poly } = proof in - let { Info.hook; scope; impargs; other_thms } = info in if List.length entries <> 1 then - user_err Pp.(str "Admitted does not support multiple statements"); + CErrors.user_err Pp.(str "Admitted does not support multiple statements"); let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in let typ = match proof_entry_type with - | None -> user_err Pp.(str "Admitted requires an explicit statement"); + | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); | Some typ -> typ in let ctx = UState.univ_entry ~poly universes in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms + finish_admitted ~name ~poly ~uctx:universes ~udecl ~info (sec_vars, (typ, ctx), None) -let save_lemma_proved_delayed ~proof ~info ~idopt = - (* Env and sigma are just used for error printing in save_remaining_recthms *) - let env = Global.env () in - let sigma = Evd.from_env env in - finalize_proof idopt env sigma proof info +let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index e790c39022..d645de1ceb 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -48,7 +48,7 @@ module Recthm : sig type t = { name : Id.t (** Name of theorem *) - ; typ : EConstr.t + ; typ : Constr.t (** Type of theorem *) ; args : Name.t list (** Names to pre-introduce *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 953faf6fdb..c78b470e3b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -15,17 +15,10 @@ open CErrors open CAst open Util open Names -open Tacmach -open Constrintern -open Prettyp open Printer open Goptions open Libnames -open Globnames open Vernacexpr -open Constrexpr -open Redexpr -open Lemmas open Locality open Attributes @@ -128,7 +121,7 @@ let show_intro ~proof all = let Proof.{goals;sigma} = Proof.data proof in if not (List.is_empty goals) then begin let gl = {Evd.it=List.hd goals ; sigma = sigma; } in - let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in + let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (Tacmach.pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in hov 0 (prlist_with_sep spc Id.print lid) @@ -493,8 +486,8 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let decl = fst (List.hd thms) in let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in - let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in + let evd, (impls, ((env, ctx), imps)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = Constrintern.interp_type_evars_impls ~program_mode ~impls env evd t in let flags = Pretyping.{ all_and_fail_flags with program_mode } in let inference_hook = if program_mode then Some program_inference_hook else None in let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in @@ -510,7 +503,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in + { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in let () = let open UState in if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then @@ -521,7 +514,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl + Lemmas.start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> @@ -587,15 +580,15 @@ let vernac_start_proof ~atts kind l = let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> - save_lemma_admitted ~lemma + Lemmas.save_lemma_admitted ~lemma | Proved (opaque,idopt) -> - save_lemma_proved ~lemma ~opaque ~idopt + Lemmas.save_lemma_proved ~lemma ~opaque ~idopt let vernac_exact_proof ~lemma c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in - let () = save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in + let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -825,7 +818,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Constrexpr.AN (qualid_of_ident ?loc id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~poly l = @@ -1543,7 +1536,7 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let glopt = query_command_selector glopt in let sigma, env = get_current_context_of_args ~pstate glopt in - let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in + let sigma, c = Constrintern.interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Evarconv.check_problems_are_solved env sigma; let sigma = Evd.minimize_universes sigma in @@ -1562,16 +1555,16 @@ let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in - print_judgment env sigma j ++ + Prettyp.print_judgment env sigma j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l | Some r -> let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in let redfun env evm c = - let (redfun, _) = reduction_of_red_expr env r_interp in + let (redfun, _) = Redexpr.reduction_of_red_expr env r_interp in let (_, c) = redfun env evm c in c in - print_eval redfun env sigma rc j + Prettyp.print_eval redfun env sigma rc j in pp ++ Printer.pr_universe_ctx_set sigma uctx @@ -1579,20 +1572,20 @@ let vernac_declare_reduction ~local s r = let local = Option.default false local in let env = Global.env () in let sigma = Evd.from_env env in - declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r)) + Redexpr.declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = let env = Global.env() in let sigma = Evd.from_env env in - let c,uctx = interp_constr env sigma c in + let c,uctx = Constrintern.interp_constr env sigma c in let senv = Global.safe_env() in let uctx = UState.context_set uctx in let senv = Safe_typing.push_context_set ~strict:false uctx senv in let c = EConstr.to_constr sigma c in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in - print_safe_judgment env sigma j ++ + Prettyp.print_safe_judgment env sigma j ++ pr_universe_ctx_set sigma uctx @@ -1618,6 +1611,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = (* FIXME error on non None udecl if we find the hyp. *) let glnumopt = query_command_selector ?loc glopt in let gl,id = + let open Constrexpr in match glnumopt, ref_or_by_not.v with | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *) (try get_nth_goal ~pstate 1, qualid_basename qid with _ -> raise NoHyp) @@ -1627,7 +1621,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in - let hyps = pf_hyps gl in + let hyps = Tacmach.pf_hyps gl in let decl = Context.Named.lookup id hyps in let natureofid = match decl with | LocalAssum _ -> "Hypothesis" @@ -1638,16 +1632,16 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = with (* fallback to globals *) | NoHyp | Not_found -> let sigma, env = get_current_or_global_context ~pstate in - print_about env sigma ref_or_by_not udecl + Prettyp.print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ env sigma - | PrintSectionContext qid -> print_sec_context_typ env sigma qid - | PrintInspect n -> inspect env sigma n + | PrintFullContext-> Prettyp.print_full_context_typ env sigma + | PrintSectionContext qid -> Prettyp.print_sec_context_typ env sigma qid + | PrintInspect n -> Prettyp.inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir @@ -1660,7 +1654,7 @@ let vernac_print ~pstate ~atts = | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name env sigma qid udecl + Prettyp.print_name env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() @@ -1692,11 +1686,11 @@ let vernac_print ~pstate ~atts = print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> dump_global qid; - print_impargs qid + Prettyp.print_impargs qid | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) let gr = smart_global r in - let cstr = printable_constr_of_global gr in + let cstr = Globnames.printable_constr_of_global gr in let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in @@ -1719,7 +1713,7 @@ open Search let interp_search_about_item env sigma = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern env sigma pat in + let _,pat = Constrintern.intern_constr_pattern env sigma pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1768,7 +1762,7 @@ let vernac_search ~pstate ~atts s gopt r = (* if goal selector is given and wrong, then let exceptions be raised. *) | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g in - let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in + let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in let pr_search ref env c = let pr = pr_global ref in let pp = if !search_output_name_only @@ -1794,17 +1788,17 @@ let vernac_search ~pstate ~atts s gopt r = (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search -let vernac_locate ~pstate = function - | LocateAny {v=AN qid} -> print_located_qualid qid - | LocateTerm {v=AN qid} -> print_located_term qid +let vernac_locate ~pstate = let open Constrexpr in function + | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid + | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *) | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = get_current_or_global_context ~pstate in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid - | LocateModule qid -> print_located_module qid - | LocateOther (s, qid) -> print_located_other s qid + | LocateModule qid -> Prettyp.print_located_module qid + | LocateOther (s, qid) -> Prettyp.print_located_other s qid | LocateFile f -> locate_file f let vernac_register qid r = |