diff options
35 files changed, 573 insertions, 383 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8b37403960..f0403a7318 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-07-09-V01" + CACHEKEY: "bionic_coq-V2019-09-20-V01" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -507,62 +507,6 @@ test-suite:egde:dune:dev: # Gitlab doesn't support yet "expire_in: never" so we use the instance default # expire_in: never -test-suite:edge+trunk+make: - stage: stage-1 - dependencies: [] - script: - - opam switch create 4.09.0 --empty - - eval $(opam env) - - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - - opam update - - opam install ocaml-variants=4.09.0+trunk - - opam pin add -n ocamlfind --dev - - opam install num - - eval $(opam env) - # We avoid problems with warnings: - - ./configure -profile devel -warn-error no - - make -j "$NJOBS" world - - make -j "$NJOBS" test-suite UNIT_TESTS= - variables: - OPAM_SWITCH: base - artifacts: - name: "$CI_JOB_NAME.logs" - when: always - paths: - - test-suite/logs - expire_in: 1 week - allow_failure: true - only: *full-ci - -test-suite:edge+trunk+dune: - stage: stage-1 - dependencies: [] - script: - - opam switch create 4.09.0 --empty - - eval $(opam env) - - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - - opam update - - opam install ocaml-variants=4.09.0+trunk - - opam pin add -n ocamlfind --dev - - opam pin add dune --dev # ounit lablgtk conf-gtksourceview - - opam install dune num - - eval $(opam env) - # We use the release profile to avoid problems with warnings - - make -f Makefile.dune trunk - - export COQ_UNIT_TEST=noop - - dune runtest --profile=ocaml409 - variables: - OPAM_SWITCH: base - artifacts: - name: "$CI_JOB_NAME.logs" - when: always - paths: - - _build/log - - _build/default/test-suite/logs - expire_in: 1 week - allow_failure: true - only: *full-ci - test-suite:base+async: extends: .test-suite-template dependencies: @@ -9,7 +9,7 @@ WHAT DO YOU NEED ? - OCaml (version >= 4.05.0) (available at https://ocaml.org/) - (This version of Coq has been tested up to OCaml 4.08.1) + (This version of Coq has been tested up to OCaml 4.09.0) - The Num package, which used to be part of the OCaml standard library, if you are using an OCaml version >= 4.06.0 diff --git a/Makefile.build b/Makefile.build index 610af5fe40..f2e1ca4ea0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -581,7 +581,7 @@ bin/votour.byte: $(VOTOURCMO) ########################################################################### CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ - mutils.cmo micromega.cmo \ + micromega.cmo mutils.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) diff --git a/Makefile.dune b/Makefile.dune index 88055d62dc..19e8a770bd 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -6,7 +6,7 @@ .PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accessory targets -.PHONY: ocheck trunk ireport clean # Maintenance targets +.PHONY: ocheck ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -36,7 +36,6 @@ help: @echo " - release: build Coq in release mode" @echo "" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" - @echo " - trunk: build with a configuration compatible with OCaml trunk" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @@ -103,11 +102,6 @@ release: voboot ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all -trunk: - dune build $(DUNEOPT) --profile=ocaml409 @vodeps - dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d - dune build $(DUNEOPT) --profile=ocaml409 coq.install coqide-server.install - ireport: dune clean dune build $(DUNEOPT) @vodeps --profile=ireport diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 84f080cc73..38ea915f3c 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -72,8 +72,8 @@ jobs: opam list displayName: 'Install OCaml dependencies' env: - COMPILER: "4.08.1" - FINDLIB_VER: ".1.8.0" + COMPILER: "4.09.0" + FINDLIB_VER: ".1.8.1" OPAMYES: "true" - script: | diff --git a/clib/hashset.ml b/clib/hashset.ml index debfc15c9a..b7a245aed1 100644 --- a/clib/hashset.ml +++ b/clib/hashset.ml @@ -118,8 +118,8 @@ module Make (E : EqType) = t.table.(t.rover) <- emptybucket; t.hashes.(t.rover) <- [| |]; end else begin - Obj.truncate (Obj.repr bucket) (prev_len + 1); - Obj.truncate (Obj.repr hbucket) prev_len; + Obj.truncate (Obj.repr bucket) (prev_len + 1) [@ocaml.alert "--deprecated"]; + Obj.truncate (Obj.repr hbucket) prev_len [@ocaml.alert "--deprecated"]; end; if len > t.limit && prev_len <= t.limit then t.oversize <- t.oversize - 1; end; diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 03ce5a6b5d..ee6c62673b 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.08.1+mingw64c +OPAM_VARIANT=ocaml-variants.4.09.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 567f0539ab..edca83c6ef 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-07-09-V01" +# CACHEKEY: "bionic_coq-V2019-09-20-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,12 +37,12 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.10.0 ounit.2.0.8 odoc.1.4.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.7.0" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" +ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" # Must add this to COQIDE_OPAM{,_EDGE} when we update the opam # packages "lablgtk3-gtksourceview3" @@ -56,9 +56,9 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.08.1" \ - COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \ - BASE_OPAM_EDGE="dune-release.1.3.1" +ENV COMPILER_EDGE="4.09.0" \ + COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \ + BASE_OPAM_EDGE="dune-release.1.3.2" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh new file mode 100644 index 0000000000..a5f6551474 --- /dev/null +++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then + + elpi_CI_REF=library+to_vernac_step2 + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 7e53f13e45..28e8773e25 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,7 +1,7 @@ -(lang dune 1.4) +(lang dune 1.10) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.08.1))) -(context (opam (switch 4.08.1+flambda))) +(context (opam (switch 4.09.0))) +(context (opam (switch 4.09.0+flambda))) diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst new file mode 100644 index 0000000000..12d8f68e63 --- /dev/null +++ b/doc/changelog/04-tactics/10765-micromega-caches.rst @@ -0,0 +1,3 @@ +- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case) + (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson). diff --git a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst new file mode 100644 index 0000000000..d6fc724415 --- /dev/null +++ b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst @@ -0,0 +1,4 @@ +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, + fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ + by Vincent Laporte). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 238106b2e7..4a691bde3a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,18 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. flag:: Lia Cache + + This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` + +.. flag:: Nia Cache + + This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache` + +.. flag:: Nra Cache + + This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache` + The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. @@ -4,9 +4,7 @@ (release (flags :standard -rectypes) (ocamlopt_flags -O3 -unbox-closures)) (ireport (flags :standard -rectypes -w -9-27-40+60) - (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)) - (ocaml409 - (flags :standard -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated))) + (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))) ; Information about flags for release mode: ; diff --git a/engine/uState.ml b/engine/uState.ml index cb40e6eadd..d93ccafcf0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -178,6 +178,7 @@ exception UniversesDiffer let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open UnivSubst in let open UnivProblem in @@ -236,22 +237,21 @@ let process_universe_constraints ctx cstrs = else match cst with | ULe (l, r) -> - if UGraph.check_leq univs l r then - (* Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) - match Universe.level l, Universe.level r with - | Some l, Some r -> - Constraint.add (l, Le, r) local - | _ -> local - else - begin match Universe.level r with - | None -> user_err Pp.(str "Algebraic universe on the right") - | Some r' -> - if Level.is_small r' then + begin match Univ.Universe.level r with + | None -> + if UGraph.check_leq univs l r then local + else user_err Pp.(str "Algebraic universe on the right") + | Some r' -> + if Level.is_small r' then if not (Universe.is_levels l) - then + then (* l contains a +1 and r=r' small so l <= r impossible *) raise (UniverseInconsistency (Le, l, r, None)) else + if UGraph.check_leq univs l r then match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> local + else let levels = Universe.levels l in let fold l' local = let l = Universe.make l' in @@ -260,8 +260,12 @@ let process_universe_constraints ctx cstrs = else raise (UniverseInconsistency (Le, l, r, None)) in LSet.fold fold levels local - else - enforce_leq l r local + else + match Univ.Universe.level l with + | Some l -> + Univ.Constraint.add (l, Le, r') local + | None -> + if UGraph.check_leq univs l r then local else enforce_leq l r local end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local diff --git a/interp/modintern.ml b/interp/modintern.ml index 955288244e..ddf5b2d7b1 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,6 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -21,9 +20,11 @@ type module_internalization_error = exception ModuleInternalizationError of module_internalization_error +type module_kind = Module | ModType | ModAny + let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = let open Declaremods in match kind with + let e = match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -46,7 +47,6 @@ let error_application_to_module_type loc = it is equal to the input kind when this one isn't ModAny. *) let lookup_module_or_modtype kind qid = - let open Declaremods in let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; diff --git a/interp/modintern.mli b/interp/modintern.mli index 75ab38c64a..72695a680e 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) +type module_kind = Module | ModType | ModAny + val interp_module_ast : - env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index e54118c775..f788832d5b 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -96,14 +96,14 @@ let mk_accu (a : atom) : t = else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Obj.repr (accumulate data) in - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in ans in let acc = { acc_atm = a; acc_arg = [] } in let ans = Obj.repr (accumulate acc) in (** FIXME: use another representation for accumulators, this causes naked pointers. *) - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in (Obj.obj ans : t) let get_accu (k : accumulator) = diff --git a/library/library.mllib b/library/library.mllib index c34d8911e8..a6188f7661 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,6 @@ Summary Nametab Global Lib -Declaremods States Kindops Goptions diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ceb651abed..1772a3c333 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -50,6 +50,13 @@ let get_lia_option () = let get_lra_option () = !lra_proof_depth +(* Enable/disable caches *) + +let use_lia_cache = ref true +let use_nia_cache = ref true +let use_nra_cache = ref true +let use_csdp_cache = ref true + let () = let int_opt l vref = @@ -88,8 +95,38 @@ let () = optwrite = (fun x -> Certificate.dump_file := x) } in + let lia_cache_opt = + { + optdepr = false; + optname = "cache of lia (.lia.cache)"; + optkey = ["Lia" ; "Cache"]; + optread = (fun () -> !use_lia_cache); + optwrite = (fun x -> use_lia_cache := x) + } in + + let nia_cache_opt = + { + optdepr = false; + optname = "cache of nia (.nia.cache)"; + optkey = ["Nia" ; "Cache"]; + optread = (fun () -> !use_nia_cache); + optwrite = (fun x -> use_nia_cache := x) + } in + + let nra_cache_opt = + { + optdepr = false; + optname = "cache of nra (.nra.cache)"; + optkey = ["Nra" ; "Cache"]; + optread = (fun () -> !use_nra_cache); + optwrite = (fun x -> use_nra_cache := x) + } in + let () = declare_bool_option solver_opt in + let () = declare_bool_option lia_cache_opt in + let () = declare_bool_option nia_cache_opt in + let () = declare_bool_option nra_cache_opt in let () = declare_stringopt_option dump_file_opt in let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in @@ -745,7 +782,7 @@ struct (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) let eq_constr gl x y = let evd = gl.sigma in - match EConstr.eq_constr_universes gl.env evd x y with + match EConstr.eq_constr_universes_proj gl.env evd x y with | Some csts -> let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in begin @@ -769,15 +806,16 @@ struct ({vars=vars';gl=gl'}, CamlToCoq.positive n) let get_rank env v = - let evd = env.gl.sigma in + let gl = env.gl in let rec _get_rank env n = match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if EConstr.eq_constr evd e v - then n - else _get_rank l (n+1) in + match eq_constr gl e v with + | Some _ -> n + | None -> _get_rank l (n+1) + in _get_rank env.vars 1 let elements env = env.vars @@ -1978,13 +2016,47 @@ type provername = string * int option open Persistent_cache -module Cache = PHashtable(struct - type t = (provername * micromega_polys) - let equal = (=) - let hash = Hashtbl.hash -end) -let csdp_cache = ".csdp.cache" +module MakeCache(T : sig type prover_option + type coeff + val hash_prover_option : int -> prover_option -> int + val hash_coeff : int -> coeff -> int + val eq_prover_option : prover_option -> prover_option -> bool + val eq_coeff : coeff -> coeff -> bool + + end) = + struct + module E = + struct + type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list + + let equal = Hash.(eq_pair T.eq_prover_option (CList.equal (eq_pair (eq_pol T.eq_coeff) Hash.eq_op1))) + + let hash = + let hash_cstr = Hash.(hash_pair (hash_pol T.hash_coeff) hash_op1) in + Hash.( (hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0) + end + + include PHashtable(E) + + let memo_opt use_cache cache_file f = + let memof = memo cache_file f in + fun x -> if !use_cache then memof x else f x + + end + + + +module CacheCsdp = MakeCache(struct + type prover_option = provername + type coeff = Mc.q + let hash_prover_option = Hash.(hash_pair hash_string + (hash_elt (Option.hash (fun x -> x)))) + let eq_prover_option = Hash.(eq_pair String.equal + (Option.equal Int.equal)) + let hash_coeff = Hash.hash_q + let eq_coeff = Hash.eq_q + end) (** * Build the command to call csdpcert, and launch it. This in turn will call @@ -2017,7 +2089,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste *) let xcall_csdpcert = - Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb) + CacheCsdp.memo_opt use_csdp_cache ".csdp.cache" (fun (prover,pb) -> really_call_csdpcert prover pb) (** * Prover callback functions. @@ -2112,23 +2184,31 @@ let compact_pt pt f = let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l) -module CacheZ = PHashtable(struct - type prover_option = bool * bool* int - type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) +module CacheZ = MakeCache(struct + type prover_option = bool * bool* int + type coeff = Mc.z + let hash_prover_option : int -> prover_option -> int = Hash.hash_elt Hashtbl.hash + let eq_prover_option : prover_option -> prover_option -> bool = (=) + let eq_coeff = Hash.eq_z + let hash_coeff = Hash.hash_z + end) -module CacheQ = PHashtable(struct - type t = int * ((Mc.q Mc.pol * Mc.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) +module CacheQ = MakeCache(struct + type prover_option = int + type coeff = Mc.q + let hash_prover_option : int -> int -> int = Hash.hash_elt Hashtbl.hash + let eq_prover_option = Int.equal + let eq_coeff = Hash.eq_q + let hash_coeff = Hash.hash_q + end) -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) -let memo_nlia = CacheZ.memo ".nia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) -let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) +let memo_lia = CacheZ.memo_opt use_lia_cache ".lia.cache" + (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) +let memo_nlia = CacheZ.memo_opt use_nia_cache ".nia.cache" + (fun ((_,ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) +let memo_nra = CacheQ.memo_opt use_nra_cache ".nra.cache" + (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) @@ -2154,63 +2234,63 @@ let linear_prover_R = { } let nlinear_prover_R = { - name = "nra"; - get_option = get_lra_option; - prover = memo_nra ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "nra"; + get_option = get_lra_option; + prover = memo_nra ; + hyps = hyps_of_cone ; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Q str o = { - name = "real nonlinear prover"; + name = "real nonlinear prover"; get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + prover = (fun (o,l) -> call_csdpcert_q o l); + hyps = hyps_of_cone; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_R str o = { - name = "real nonlinear prover"; - get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> call_csdpcert_q o l); - hyps = hyps_of_cone; - compact = compact_cone; - pp_prf = pp_psatz pp_q; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "real nonlinear prover"; + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> call_csdpcert_q o l); + hyps = hyps_of_cone; + compact = compact_cone; + pp_prf = pp_psatz pp_q; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Z str o = { - name = "real nonlinear prover"; + name = "real nonlinear prover"; get_option = (fun () -> (str,o)); - prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + name = "lia"; + get_option = get_lia_option; + prover = memo_lia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } let nlinear_Z = { - name = "nlia"; - get_option = get_lia_option; - prover = memo_nlia ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) + name = "nlia"; + get_option = get_lia_option; + prover = memo_nlia ; + hyps = hyps_of_pt; + compact = compact_pt; + pp_prf = pp_proof_term; + pp_f = fun o x -> pp_pol pp_z o (fst x) } (** diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 537b6175b4..39905f8c52 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -233,6 +233,13 @@ struct | Zpos p -> (positive_big_int p) | Zneg p -> minus_big_int (positive_big_int p) + let z x = + match x with + | Z0 -> 0 + | Zpos p -> index p + | Zneg p -> - (index p) + + let q_to_num {qnum = x ; qden = y} = Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y))) @@ -420,6 +427,80 @@ let command exe_path args vl = stdout_read; stdout_write; stderr_read; stderr_write]) +(** Hashing utilities *) + +module Hash = + struct + + module Mc = Micromega + + open Hashset.Combine + + let int_of_eq_op1 = Mc.(function + | Equal -> 0 + | NonEqual -> 1 + | Strict -> 2 + | NonStrict -> 3) + + let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2 + + let hash_op1 h o = combine h (int_of_eq_op1 o) + + + let rec eq_positive p1 p2 = + match p1 , p2 with + | Mc.XH , Mc.XH -> true + | Mc.XI p1 , Mc.XI p2 -> eq_positive p1 p2 + | Mc.XO p1 , Mc.XO p2 -> eq_positive p1 p2 + | _ , _ -> false + + let eq_z z1 z2 = + match z1 , z2 with + | Mc.Z0 , Mc.Z0 -> true + | Mc.Zpos p1, Mc.Zpos p2 + | Mc.Zneg p1, Mc.Zneg p2 -> eq_positive p1 p2 + | _ , _ -> false + + let eq_q {Mc.qnum = qn1 ; Mc.qden = qd1} {Mc.qnum = qn2 ; Mc.qden = qd2} = + eq_z qn1 qn2 && eq_positive qd1 qd2 + + let rec eq_pol eq p1 p2 = + match p1 , p2 with + | Mc.Pc c1 , Mc.Pc c2 -> eq c1 c2 + | Mc.Pinj(i1,p1) , Mc.Pinj(i2,p2) -> eq_positive i1 i2 && eq_pol eq p1 p2 + | Mc.PX(p1,i1,p1') , Mc.PX(p2,i2,p2') -> + eq_pol eq p1 p2 && eq_positive i1 i2 && eq_pol eq p1' p2' + | _ , _ -> false + + + let eq_pair eq1 eq2 (x1,y1) (x2,y2) = + eq1 x1 x2 && eq2 y1 y2 + + + let hash_pol helt = + let rec hash acc = function + | Mc.Pc c -> helt (combine acc 1) c + | Mc.Pinj(p,c) -> hash (combine (combine acc 1) (CoqToCaml.index p)) c + | Mc.PX(p1,i,p2) -> hash (hash (combine (combine acc 2) (CoqToCaml.index i)) p1) p2 in + hash + + + let hash_pair h1 h2 h (e1,e2) = + h2 (h1 h e1) e2 + + let hash_elt f h e = combine h (f e) + + let hash_string h (e:string) = hash_elt Hashtbl.hash h e + + let hash_z = hash_elt CoqToCaml.z + + let hash_q = hash_elt (fun q -> Hashtbl.hash (CoqToCaml.q_to_num q)) + + end + + + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 8dbdea39e2..9692bc631b 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -67,14 +67,46 @@ end module CoqToCaml : sig val z_big_int : Micromega.z -> Big_int.big_int - val q_to_num : Micromega.q -> Num.num - val positive : Micromega.positive -> int - val n : Micromega.n -> int - val nat : Micromega.nat -> int - val index : Micromega.positive -> int + val z : Micromega.z -> int + val q_to_num : Micromega.q -> Num.num + val positive : Micromega.positive -> int + val n : Micromega.n -> int + val nat : Micromega.nat -> int + val index : Micromega.positive -> int end +module Hash : sig + + val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool + + val eq_positive : Micromega.positive -> Micromega.positive -> bool + + val eq_z : Micromega.z -> Micromega.z -> bool + + val eq_q : Micromega.q -> Micromega.q -> bool + + val eq_pol : ('a -> 'a -> bool) -> 'a Micromega.pol -> 'a Micromega.pol -> bool + + val eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a * 'b -> 'a * 'b -> bool + + val hash_op1 : int -> Micromega.op1 -> int + + val hash_pol : (int -> 'a -> int) -> int -> 'a Micromega.pol -> int + + val hash_pair : (int -> 'a -> int) -> (int -> 'b -> int) -> int -> 'a * 'b -> int + + val hash_z : int -> Micromega.z -> int + + val hash_q : int -> Micromega.q -> int + + val hash_string : int -> string -> int + + val hash_elt : ('a -> int) -> int -> 'a -> int + +end + + val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 14a1bc9712..14e2e40846 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -127,7 +127,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.replace htbl key elem ; + Table.add htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -164,7 +164,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.replace tbl k e ; + Table.add tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fb0b1eca8d..c995887f31 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -38,11 +38,11 @@ type object_pr = { print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -618,7 +618,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -639,17 +639,17 @@ let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module with_values (MPdot (mp,l))) + Some (print_module ~mod_ops with_values (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype (MPdot (mp,l))) + Some (print_modtype ~mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry indirect_accessor env sigma with_values ent = +let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -657,10 +657,10 @@ let gallina_print_library_entry indirect_accessor env sigma with_values ent = | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context indirect_accessor env sigma with_values = +let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry indirect_accessor env sigma with_values h with + (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -698,8 +698,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry x = !object_pr.print_library_entry x -let print_context x = !object_pr.print_context x +let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x +let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -720,10 +720,12 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) -let print_full_pure_context ~library_accessor env sigma = +let print_full_pure_context ~mod_ops ~library_accessor env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -758,11 +760,11 @@ let print_full_pure_context ~library_accessor env sigma = | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -787,11 +789,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context indirect_accessor env sigma sec = - print_context indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) -let print_sec_context_typ indirect_accessor env sigma sec = - print_context indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -801,7 +803,7 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name indirect_accessor env sigma na udecl = +let print_any_name ~mod_ops indirect_accessor env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with @@ -810,9 +812,10 @@ let print_any_name indirect_accessor env sigma na udecl = | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn - | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp + | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> + print_module ~mod_ops (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype mp + | ModuleType mp -> print_modtype ~mod_ops mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -824,15 +827,15 @@ let print_any_name indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name indirect_accessor env sigma na udecl = +let print_name ~mod_ops indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name indirect_accessor env sigma + print_any_name ~mod_ops indirect_accessor env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl let print_opaque_name indirect_accessor env sigma qid = let open GlobRef in @@ -888,8 +891,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect indirect_accessor env sigma depth = - print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect ~mod_ops indirect_accessor env sigma depth = + print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 4299bcc880..c8b361d95b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,28 +19,35 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option val print_full_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_full_pure_context - : library_accessor:Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> library_accessor:Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t val print_sec_context - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_sec_context_typ - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : @@ -48,7 +55,8 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name - : Opaqueproof.indirect_accessor + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_opaque_name @@ -69,7 +77,10 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t +val inspect + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -105,11 +116,11 @@ type object_pr = { print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : bool -> ModPath.t -> Pp.t; - print_modtype : ModPath.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 141469ff9c..03921bca30 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -240,9 +240,14 @@ let nametab_register_body mp dir (l,body) = mip.mind_consnames) mib.mind_packets -let nametab_register_module_body mp struc = +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +let nametab_register_module_body ~mod_ops mp struc = (* If [mp] is a globally visible module, we simply import it *) - try Declaremods.import_module ~export:false mp + try mod_ops.import_module ~export:false mp with Not_found -> (* Otherwise we try to emulate an import by playing with nametab *) nametab_register_dir mp; @@ -252,7 +257,7 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with | Some (NoFunctor me) -> me | _ -> raise Not_found -let nametab_register_modparam mbid mtb = +let nametab_register_modparam ~mod_ops mbid mtb = let id = MBId.to_id mbid in match mtb.mod_type with | MoreFunctor _ -> id (* functorial param : nothing to register *) @@ -260,7 +265,7 @@ let nametab_register_modparam mbid mtb = (* We first try to use the algebraic type expression if any, via a Declaremods function that converts back to module entries *) try - let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in + let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in id with e when CErrors.noncritical e -> (* Otherwise, we try to play with the nametab ourselves *) @@ -314,9 +319,9 @@ let print_body is_impl extent env mp (l,body) = let print_struct is_impl extent env mp struc = prlist_with_sep spc (print_body is_impl extent env mp) struc -let print_structure is_type extent env mp locals struc = +let print_structure ~mod_ops is_type extent env mp locals struc = let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in - nametab_register_module_body mp struc; + nametab_register_module_body ~mod_ops mp struc; let kwd = if is_type then "Sig" else "Struct" in hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ brk (1,-2) ++ keyword "End") @@ -362,31 +367,31 @@ let print_mod_expr env mp locals = function (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") | MEwith _ -> assert false (* No 'with' syntax for modules *) -let rec print_functor fty fatom is_type extent env mp locals = function - | NoFunctor me -> fatom is_type extent env mp locals me +let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function + | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me | MoreFunctor (mbid,mtb1,me2) -> - let id = nametab_register_modparam mbid mtb1 in + let id = nametab_register_modparam ~mod_ops mbid mtb1 in let mp1 = MPbound mbid in - let pr_mtb1 = fty extent env mp1 locals mtb1 in + let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in let env' = Modops.add_module_type mp1 mtb1 env in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ - spc() ++ print_functor fty fatom is_type extent env' mp locals' me2) + spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) -let rec print_expression x = - print_functor +let rec print_expression ~mod_ops x = + print_functor ~mod_ops print_modtype - (function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x + (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x -and print_signature x = - print_functor print_modtype print_structure x +and print_signature ~mod_ops x = + print_functor ~mod_ops print_modtype print_structure x -and print_modtype extent env mp locals mtb = match mtb.mod_type_alg with - | Some me -> print_expression true extent env mp locals me - | None -> print_signature true extent env mp locals mtb.mod_type +and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with + | Some me -> print_expression ~mod_ops true extent env mp locals me + | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type let rec printable_body dir = let dir = pop_dirpath dir in @@ -403,52 +408,52 @@ let rec printable_body dir = (** Since we might play with nametab above, we should reset to prior state after the printing *) -let print_expression' is_type extent env mp me = +let print_expression' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_expression is_type extent env mp [] e) me + (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me -let print_signature' is_type extent env mp me = +let print_signature' ~mod_ops is_type extent env mp me = States.with_state_protection - (fun e -> print_signature is_type extent env mp [] e) me + (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me -let unsafe_print_module extent env mp with_body mb = +let unsafe_print_module ~mod_ops extent env mp with_body mb = let name = print_modpath [] mp in let pr_equals = spc () ++ str ":= " in let body = match with_body, mb.mod_expr with | false, _ | true, Abstract -> mt() - | _, Algebraic me -> pr_equals ++ print_expression' false extent env mp me - | _, Struct sign -> pr_equals ++ print_signature' false extent env mp sign - | _, FullStruct -> pr_equals ++ print_signature' false extent env mp mb.mod_type + | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me + | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign + | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type in let modtype = match mb.mod_expr, mb.mod_type_alg with | FullStruct, _ -> mt () - | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true extent env mp ty - | _, _ -> brk (1,1) ++ str": " ++ print_signature' true extent env mp mb.mod_type + | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty + | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type in hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body) exception ShortPrinting -let print_module with_body mp = +let print_module ~mod_ops with_body mp = let me = Global.lookup_module mp in try if !short then raise ShortPrinting; - unsafe_print_module WithContents + unsafe_print_module ~mod_ops WithContents (Global.env ()) mp with_body me ++ fnl () with e when CErrors.noncritical e -> - unsafe_print_module OnlyNames + unsafe_print_module ~mod_ops OnlyNames (Global.env ()) mp with_body me ++ fnl () -let print_modtype kn = +let print_modtype ~mod_ops kn = let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in hv 1 (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++ try if !short then raise ShortPrinting; - print_signature' true WithContents + print_signature' ~mod_ops true WithContents (Global.env ()) kn mtb.mod_type with e when CErrors.noncritical e -> - print_signature' true OnlyNames + print_signature' ~mod_ops true OnlyNames (Global.env ()) kn mtb.mod_type) diff --git a/printing/printmod.mli b/printing/printmod.mli index 8fd1cb4183..4c9245ee27 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -16,5 +16,11 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> UnivNames.univ_name_list option -> Pp.t -val print_module : bool -> ModPath.t -> Pp.t -val print_modtype : ModPath.t -> Pp.t + +type mod_ops = + { import_module : export:bool -> ModPath.t -> unit + ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + } + +val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t +val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v new file mode 100644 index 0000000000..25285622a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9512.v @@ -0,0 +1,35 @@ +Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia. + +Set Primitive Projections. +Record params := { width : Z }. +Definition p : params := Build_params 64. + +Set Printing All. + +Goal width p = 0%Z -> width p = 0%Z. + intros. + + assert_succeeds (enough True; [omega|]). + assert_succeeds (enough True; [lia|]). + +(* H : @eq Z (width p) Z0 *) +(* ============================ *) +(* @eq Z (width p) Z0 *) + + change tt with tt in H. + +(* H : @eq Z (width p) Z0 *) +(* ============================ *) +(* @eq Z (width p) Z0 *) + + assert_succeeds (enough True; [lia|]). + (* Tactic failure: <tactic closure> fails. *) + (* assert_succeeds (enough True; [omega|]). *) + (* Tactic failure: <tactic closure> fails. *) + + (* omega. *) + (* Error: Omega can't solve this system *) + + lia. + (* Tactic failure: Cannot find witness. *) +Qed. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index 74f94a9bed..d293dc0533 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -196,7 +196,7 @@ Definition clone_subType U v := Variable sT : subType. -CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). +Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). Lemma SubP u : Sub_spec u. Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. @@ -209,7 +209,7 @@ Definition insub x := Definition insubd u0 x := odflt u0 (insub x). -CoInductive insub_spec x : option sT -> Type := +Variant insub_spec x : option sT -> Type := | InsubSome u of P x & val u = x : insub_spec x (Some u) | InsubNone of ~~ P x : insub_spec x None. @@ -568,7 +568,7 @@ Fixpoint nth s n {struct n} := Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z]. -CoInductive last_spec : seq T -> Type := +Variant last_spec : seq T -> Type := | LastNil : last_spec [::] | LastRcons s x : last_spec (rcons s x). @@ -1292,7 +1292,7 @@ Open Scope big_scope. (* packages both in in a term in which i occurs; it also depends on the *) (* iterated <op>, as this can give more information on the expected type of *) (* the <general_term>, thus allowing for the insertion of coercions. *) -CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R. +Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R. Definition applybig {R I} (body : bigbody R I) x := let: BigBody _ op b v := body in if b then op v x else x. diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7658ad68a5..642dc94ab2 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -54,7 +54,10 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in let library_accessor = Library.indirect_accessor in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ()) + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/library/declaremods.ml b/vernac/declaremods.ml index b4dc42bdfe..58a7dff5fd 100644 --- a/library/declaremods.ml +++ b/vernac/declaremods.ml @@ -35,8 +35,6 @@ type inline = | DefaultInline | InlineAt of int -type module_kind = Module | ModType | ModAny - let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function @@ -457,15 +455,15 @@ let rec compute_subst env mbids sign mp_l inl = | _,[] -> mbids,empty_subst | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in + let mb = Environ.lookup_module mp env in + let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in + let resolver = if Modops.is_functor mb.mod_type then empty_delta_resolver else Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - in - mbid_left,join (map_mbid mbid mp resolver) subst + in + mbid_left,join (map_mbid mbid mp resolver) subst (** Create the objects of a "with Module" structure. *) @@ -547,11 +545,11 @@ let process_module_binding mbid me = Objects in these parameters are also loaded. Output is accumulated on top of [acc] (in reverse order). *) -let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = +let intern_arg (acc, cst) (idl,(typ,ann)) = let inl = inl2intopt ann in let lib_dir = Lib.library_dp() in let env = Global.env() in - let (mty, _, cst') = interp_modast env ModType typ in + let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in let () = Global.push_context_set true cst' in let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in @@ -579,8 +577,8 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = be more efficient and independent of [List.map] eval order. *) -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params +let intern_args params = + List.fold_left intern_arg ([], Univ.ContextSet.empty) params (** {6 Auxiliary functions concerning subtyping checks} *) @@ -588,10 +586,10 @@ let intern_args interp_modast params = let check_sub mtb sub_mtb_l = (* The constraints are checked and forgot immediately : *) ignore (List.fold_right - (fun sub_mtb env -> - Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) env) - sub_mtb_l (Global.env())) + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (Global.env())) (** This function checks if the type calculated for the module [mp] is a subtype of all signatures in [sub_mtb_l]. Uses only the global @@ -631,11 +629,11 @@ let mk_funct_type env args seb0 = (** Prepare the module type list for check of subtypes *) -let build_subtypes interp_modast env mp args mtys = +let build_subtypes env mp args mtys = let (cst, ans) = List.fold_left_map (fun cst (m,ann) -> let inl = inl2intopt ann in - let mte, _, cst' = interp_modast env ModType m in + let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in let env = Environ.push_context_set ~strict:true cst' env in let cst = Univ.ContextSet.union cst cst' in let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in @@ -673,22 +671,22 @@ let openmodtype_info = module RawModOps = struct -let start_module interp_modast export id args res fs = +let start_module export id args res fs = let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType res in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in let cst = Univ.ContextSet.union cst cst' in Some (mte, inl), [], cst | Check resl -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in + let typs, cst = build_subtypes env mp arg_entries_r resl in None, typs, cst in let () = Global.push_context_set true cst in @@ -735,25 +733,25 @@ let end_module () = mp -let declare_module interp_modast id args res mexpr_o fs = +let declare_module id args res mexpr_o fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let params = mk_params_entry arg_entries_r in let env = Global.env () in let env = Environ.push_context_set ~strict:true cst env in let mty_entry_o, subs, inl_res, cst' = match res with | Enforce (mty,ann) -> let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType mty in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in let env = Environ.push_context_set ~strict:true cst env in (* We check immediately that mte is well-formed *) let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in let cst = Univ.ContextSet.union cst cst' in Some mte, [], inl, cst | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let typs, cst = build_subtypes env mp arg_entries_r mtys in None, typs, default_inline (), cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -761,7 +759,7 @@ let declare_module interp_modast id args res mexpr_o fs = let mexpr_entry_o, inl_expr, cst' = match mexpr_o with | None -> None, default_inline (), Univ.ContextSet.empty | Some (mexpr,ann) -> - let (mte, _, cst) = interp_modast env Module mexpr in + let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in Some mte, inl2intopt ann, cst in let env = Environ.push_context_set ~strict:true cst' env in @@ -803,12 +801,12 @@ end module RawModTypeOps = struct -let start_modtype interp_modast id args mtys fs = +let start_modtype id args mtys fs = let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let env = Global.env () in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in let () = Global.push_context_set true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in @@ -831,16 +829,16 @@ let end_modtype () = mp -let declare_modtype interp_modast id args mtys (mty,ann) fs = +let declare_modtype id args mtys (mty,ann) fs = let inl = inl2intopt ann in (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in + let arg_entries_r, cst = intern_args args in let () = Global.push_context_set true cst in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mte, _, cst = interp_modast env ModType mty in + let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in let () = Global.push_context_set true cst in let env = Global.env () in (* We check immediately that mte is well-formed *) @@ -848,7 +846,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let () = Global.push_context_set true cst in let env = Global.env () in let entry = params, mte in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in + let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in let () = Global.push_context_set true cst in let env = Global.env () in let sobjs = get_functor_sobjs false env inl entry in @@ -902,12 +900,12 @@ let type_of_incl env is_mod = function decompose_functor mp_l (type_of_mod mp0 env is_mod) |MEwith _ -> raise NoIncludeSelf -let declare_one_include interp_modast (me_ast,annot) = +let declare_one_include (me_ast,annot) = let env = Global.env() in - let me, kind, cst = interp_modast env ModAny me_ast in + let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in let () = Global.push_context_set true cst in let env = Global.env () in - let is_mod = (kind == Module) in + let is_mod = (kind == Modintern.Module) in let cur_mp = Lib.current_mp () in let inl = inl2intopt annot in let mbids,aobjs = get_module_sobjs is_mod env inl me in @@ -925,8 +923,7 @@ let declare_one_include interp_modast (me_ast,annot) = let aobjs = subst_aobjs subst aobjs in ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts +let declare_include me_asts = List.iter declare_one_include me_asts end @@ -942,40 +939,40 @@ let protect_summaries f = let () = Summary.unfreeze_summaries fs in iraise reraise -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) +let start_module export id args res = + protect_summaries (RawModOps.start_module export id args res) let end_module = RawModOps.end_module -let declare_module interp id args mtys me_l = +let declare_module id args mtys me_l = let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs + | [] -> RawModOps.declare_module id args mtys None fs + | [me] -> RawModOps.declare_module id args mtys (Some me) fs | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; - RawModOps.end_module () + ignore (RawModOps.start_module None id args mtys fs); + RawIncludeOps.declare_include me_l; + RawModOps.end_module () in protect_summaries declare_me -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) +let start_modtype id args mtys = + protect_summaries (RawModTypeOps.start_modtype id args mtys) let end_modtype = RawModTypeOps.end_modtype -let declare_modtype interp id args mtys mty_l = +let declare_modtype id args mtys mty_l = let declare_mt fs = match mty_l with | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs + | [mty] -> RawModTypeOps.declare_modtype id args mtys mty fs | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; - RawModTypeOps.end_modtype () + ignore (RawModTypeOps.start_modtype id args mtys fs); + RawIncludeOps.declare_include mty_l; + RawModTypeOps.end_modtype () in protect_summaries declare_mt -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) +let declare_include me_asts = + protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts) (** {6 Libraries} *) @@ -1055,12 +1052,7 @@ let iter_all_segments f = (** {6 Some types used to shorten declaremods.mli} *) -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list +type module_params = (lident list * (Constrexpr.module_ast * inline)) list (** {6 Debug} *) diff --git a/library/declaremods.mli b/vernac/declaremods.mli index b7c7cd1dba..ae84704656 100644 --- a/library/declaremods.mli +++ b/vernac/declaremods.mli @@ -29,34 +29,24 @@ type inline = (** Kinds of modules *) -type module_kind = Module | ModType | ModAny +type module_params = (lident list * (Constrexpr.module_ast * inline)) list -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) +(** [declare_module id fargs typ exprs] declares module [id], from + functor arguments [fargs], with final type [typ]. [exprs] is + usually of length 1 (Module definition with a concrete body), but + it could also be empty ("Declare Module", with non-empty [typ]), or + multiple (body of the shape M <+ N <+ ...). *) val declare_module : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_module : - 'modast module_interpretor -> bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> ModPath.t val end_module : unit -> ModPath.t @@ -68,18 +58,16 @@ val end_module : unit -> ModPath.t Similar to [declare_module], except that the types could be multiple *) val declare_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> + module_params -> + (Constrexpr.module_ast * inline) list -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) list -> ModPath.t val end_modtype : unit -> ModPath.t @@ -117,8 +105,7 @@ val import_modules : export:bool -> ModPath.t list -> unit (** Include *) -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit +val declare_include : (Constrexpr.module_ast * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ea34b601e8..c335d3ad55 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1079,9 +1079,7 @@ let explain_incorrect_with_in_module () = let explain_incorrect_module_application () = str "Illegal application to a module type." -open Modintern - -let explain_module_internalization_error = function +let explain_module_internalization_error = let open Modintern in function | NotAModuleNorModtype s -> explain_not_module_nor_modtype s | IncorrectWithInModule -> explain_incorrect_with_in_module () | IncorrectModuleApplication -> explain_incorrect_module_application () diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index cd13f83e96..4868182bb3 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,6 +1,7 @@ Vernacexpr Attributes Pvernac +Declaremods G_vernac G_proofs Vernacprop diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c3be57eec8..bc47ad8699 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -872,10 +872,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Declaremods.Enforce mty_ast) [] - in + let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export @@ -892,10 +889,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_module Modintern.interp_module_ast - export id binders_ast mty_ast_o - in + let mp = Declaremods.start_module export id binders_ast mty_ast_o in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Interactive Module " ++ Id.print id ++ str " started"); @@ -911,7 +905,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = - Declaremods.declare_module Modintern.interp_module_ast + Declaremods.declare_module id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef ?loc mp "mod"; @@ -938,10 +932,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in - let mp = - Declaremods.start_modtype Modintern.interp_module_ast - id binders_ast mty_sign - in + let mp = Declaremods.start_modtype id binders_ast mty_sign in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Interactive Module Type " ++ Id.print id ++ str " started"); @@ -957,10 +948,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if not (Option.is_empty export) then user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - let mp = - Declaremods.declare_modtype Modintern.interp_module_ast - id binders_ast mty_sign mty_ast_l - in + let mp = Declaremods.declare_modtype id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") @@ -970,8 +958,7 @@ let vernac_end_modtype {loc;v=id} = Dumpglob.dump_modref ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") -let vernac_include l = - Declaremods.declare_include Modintern.interp_module_ast l +let vernac_include l = Declaremods.declare_include l (**********************) (* Gallina extensions *) @@ -1968,26 +1955,29 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = + let mod_ops = { Printmod.import_module = Declaremods.import_module + ; process_module_binding = Declaremods.process_module_binding + } in 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 Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma + | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid + | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module qid - | PrintModuleType qid -> print_modtype qid + | PrintModule qid -> print_module ~mod_ops qid + | PrintModuleType qid -> print_modtype ~mod_ops qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name Library.indirect_accessor env sigma qid udecl + print_name ~mod_ops Library.indirect_accessor env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() |