diff options
158 files changed, 2801 insertions, 1249 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3a626796a6..c3e59a6d89 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -62,6 +62,7 @@ before_script: # TODO figure out how to build doc for installed Coq .build-template: stage: stage-1 + interruptible: true artifacts: name: "$CI_JOB_NAME" paths: @@ -98,6 +99,7 @@ before_script: # Template for building Coq + stdlib, typical use: overload the switch .dune-template: stage: stage-1 + interruptible: true dependencies: [] script: - set -e @@ -117,6 +119,7 @@ before_script: .dune-ci-template: stage: stage-2 + interruptible: true needs: - build:edge+flambda:dune:dev dependencies: @@ -143,6 +146,7 @@ before_script: .doc-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -158,6 +162,7 @@ before_script: # set dependencies when using .test-suite-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -179,6 +184,7 @@ before_script: # set dependencies when using .validate-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -195,6 +201,7 @@ before_script: .ci-template: stage: stage-2 + interruptible: true script: - set -e - echo 'start:coq.test' @@ -218,6 +225,7 @@ before_script: .windows-template: stage: stage-1 + interruptible: true artifacts: name: "%CI_JOB_NAME%" paths: @@ -226,7 +234,7 @@ before_script: expire_in: 1 week dependencies: [] tags: - - windows + - windows-inria before_script: [] script: - call dev/ci/gitlab.bat @@ -320,6 +328,7 @@ lint: pkg:opam: stage: stage-1 + interruptible: true # OPAM will build out-of-tree so no point in importing artifacts dependencies: [] script: @@ -336,6 +345,7 @@ pkg:opam: .nix-template: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git + interruptible: true stage: stage-1 variables: # By default we use coq.cachix.org as an extra substituter but this can be overridden diff --git a/Makefile.build b/Makefile.build index 5b879220d0..a8ae040f8e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -840,7 +840,7 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) $(SHOW)'COQC -quick -noinit $<' - $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -vio -noglob # The general rule for building .vo files : @@ -855,8 +855,8 @@ ifdef VALIDATE endif %.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP) - $(SHOW)'COQC -quick $<' - $(HIDE)$(BOOTCOQC) $< -quick -noglob + $(SHOW)'COQC -vio $<' + $(HIDE)$(BOOTCOQC) $< -vio -noglob %.v.timing.diff: %.v.before-timing %.v.after-timing $(SHOW)PYTHON TIMING-DIFF $< diff --git a/Makefile.doc b/Makefile.doc index 125a4b33d5..50c4acb416 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -129,6 +129,8 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst) # Standard library ###################################################################### +DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 + ### Standard library (browsable html format) ifdef QUICK @@ -139,7 +141,7 @@ endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ - -R theories Coq -R plugins Coq $(VFILES) + $(DOCLIBS) $(VFILES) mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index @@ -178,12 +180,12 @@ doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp endif diff --git a/Makefile.dune b/Makefile.dune index bafb40d55f..b433ed1b94 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 ireport clean # Maintenance targets +.PHONY: fmt ocheck ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -36,6 +36,7 @@ help: @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @echo "" + @echo " - fmt: run ocamlformat on the codebase" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @@ -100,6 +101,9 @@ apidoc: voboot release: voboot dune build $(DUNEOPT) -p coq +fmt: voboot + dune build @fmt + ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all @@ -31,6 +31,9 @@ environment for semi-interactive development of machine-checked proofs. [![Homebrew package][homebrew-badge]][homebrew-link] [![nixpkgs unstable package][nixpkgs-badge]][nixpkgs-link] +[![Docker Hub package][dockerhub-badge]][dockerhub-link] +[![latest dockerized version][coqorg-badge]][coqorg-link] + [repology-badge]: https://repology.org/badge/latest-versions/coq.svg [repology-link]: https://repology.org/metapackage/coq/versions @@ -52,6 +55,12 @@ environment for semi-interactive development of machine-checked proofs. [nixpkgs-badge]: https://repology.org/badge/version-for-repo/nix_unstable/coq.svg [nixpkgs-link]: https://nixos.org/nixos/packages.html#coq +[dockerhub-badge]: https://img.shields.io/docker/automated/coqorg/coq.svg +[dockerhub-link]: https://hub.docker.com/r/coqorg/coq "Automated build on Docker Hub" + +[coqorg-badge]: https://images.microbadger.com/badges/version/coqorg/coq.svg +[coqorg-link]: https://github.com/coq-community/docker-coq/wiki#docker-coq-images "Docker images of Coq" + Download the pre-built packages of the [latest release][] for Windows and macOS; read the [help page][opam-using] on how to install Coq with OPAM; or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source. diff --git a/checker/check.ml b/checker/check.ml index ffb2928d55..4ac5c56732 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -294,14 +294,22 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe (* Dependency graph *) let depgraph = ref LibraryMap.empty -let marshal_in_segment f ch = - try - let stop = input_binary_int ch in - let v = Analyze.instantiate (Analyze.parse_channel ch) in - let digest = Digest.input ch in +let marshal_in_segment ~validate ~value f ch = + if validate then + let v, stop, digest = + try + let stop = input_binary_int ch in + let v = Analyze.parse_channel ch in + let digest = Digest.input ch in + v, stop, digest + with _ -> + user_err (str "Corrupted file " ++ quote (str f)) + in + let () = Validate.validate ~debug:!Flags.debug value v in + let v = Analyze.instantiate v in Obj.obj v, stop, digest - with _ -> - user_err (str "Corrupted file " ++ quote (str f)) + else + System.marshal_in_segment f ch let skip_in_segment f ch = try @@ -312,30 +320,26 @@ let skip_in_segment f ch = with _ -> user_err (str "Corrupted file " ++ quote (str f)) -let marshal_or_skip ~intern_mode f ch = - if intern_mode <> Dep then - let v, pos, digest = marshal_in_segment f ch in +let marshal_or_skip ~validate ~value f ch = + if validate then + let v, pos, digest = marshal_in_segment ~validate ~value f ch in Some v, pos, digest else let pos, digest = skip_in_segment f ch in None, pos, digest let intern_from_file ~intern_mode (dir, f) = - let validate a b c = if intern_mode <> Dep then Validate.validate a b c in + let validate = intern_mode <> Dep in Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try - let marshal_in_segment f ch = if intern_mode <> Dep - then marshal_in_segment f ch - else System.marshal_in_segment f ch - in let ch = System.with_magic_number_check raw_intern_library f in - let (sd:summary_disk), _, digest = marshal_in_segment f ch in - let (md:library_disk), _, digest = marshal_in_segment f ch in - let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in - let (tasks:'a option), _, _ = marshal_in_segment f ch in + let (sd:summary_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_libsum f ch in + let (md:library_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_lib f ch in + let (opaque_csts:seg_univ option), _, udg = marshal_in_segment ~validate ~value:Values.v_univopaques f ch in + let (tasks:'a option), _, _ = marshal_in_segment ~validate ~value:Values.(Opt Any) f ch in let (table:seg_proofs option), pos, checksum = - marshal_or_skip ~intern_mode f ch in + marshal_or_skip ~validate ~value:Values.v_opaquetable f ch in (* Verification of the final checksum *) let () = close_in ch in let ch = open_in_bin f in @@ -354,12 +358,7 @@ let intern_from_file ~intern_mode (dir, f) = user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; - validate !Flags.debug Values.v_univopaques opaque_csts; end; - (* Verification of the unmarshalled values *) - validate !Flags.debug Values.v_libsum sd; - validate !Flags.debug Values.v_lib md; - validate !Flags.debug Values.(Opt v_opaquetable) table; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = if opaque_csts <> None then Safe_typing.Dvivo (digest,udg) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 06ee4fcc7a..e606d60d96 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -73,7 +73,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) - | (RegularArity _ | TemplateArity _), _ -> false + | (RegularArity _ | TemplateArity _), _ -> assert false let check_kelim k1 k2 = Sorts.family_leq k1 k2 @@ -139,7 +139,7 @@ let check_inductive env mind mb = let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; - mind_universes; mind_variance; + mind_universes; mind_variance; mind_sec_variance; mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) @@ -148,7 +148,7 @@ let check_inductive env mind mb = check_positive = mb_flags.check_positive; check_universes = mb_flags.check_universes; conv_oracle = mb_flags.conv_oracle} env in - Indtypes.check_inductive env mind entry + Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in @@ -165,7 +165,9 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) - ignore mind_variance; (* Indtypes did the necessary checking *) + check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal) + mb.mind_variance mind_variance); + check "mind_sec_variance" (Option.is_empty mind_sec_variance); ignore mind_private; (* passed through Indtypes *) ignore mind_typing_flags; diff --git a/checker/validate.ml b/checker/validate.ml index 070a112bb6..6ffc43394b 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -8,32 +8,39 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Analyze + (* This module defines validation functions to ensure an imported value (using input_value) has the correct structure. *) -let rec pr_obj_rec o = - if Obj.is_int o then - Format.print_int(Obj.magic o) - else if Obj.is_block o then - let t = Obj.tag o in - if t > Obj.no_scan_tag then - if t = Obj.string_tag then - Format.print_string ("\""^String.escaped(Obj.magic o)^"\"") - else - Format.print_string "?" - else - (let n = Obj.size o in - Format.print_string ("#"^string_of_int t^"("); - Format.open_hvbox 0; - for i = 0 to n-1 do - pr_obj_rec (Obj.field o i); - if i<>n-1 then (Format.print_string ","; Format.print_cut()) - done; - Format.close_box(); - Format.print_string ")") - else Format.print_string "?" - -let pr_obj o = pr_obj_rec o; Format.print_newline() +let rec pr_obj_rec mem o = match o with +| Int i -> + Format.print_int i +| Ptr p -> + let v = LargeArray.get mem p in + begin match v with + | Struct (tag, data) -> + let n = Array.length data in + Format.print_string ("#"^string_of_int tag^"("); + Format.open_hvbox 0; + for i = 0 to n-1 do + pr_obj_rec mem (Array.get data i); + if i<>n-1 then (Format.print_string ","; Format.print_cut()) + done; + Format.close_box(); + Format.print_string ")" + | String s -> + Format.print_string ("\""^String.escaped s^"\"") + | Int64 _ + | Float64 _ -> + Format.print_string "?" + end +| Atm tag -> + Format.print_string ("#"^string_of_int tag^"()"); +| Fun addr -> + Format.printf "fun@%x" addr + +let pr_obj mem o = pr_obj_rec mem o; Format.print_newline() (**************************************************************************) (* Obj low-level validators *) @@ -48,63 +55,115 @@ type error_context = error_frame list let mt_ec : error_context = [] let (/) (ctx:error_context) s : error_context = s::ctx -exception ValidObjError of string * error_context * Obj.t -let fail ctx o s = raise (ValidObjError(s,ctx,o)) +exception ValidObjError of string * error_context * data +let fail _mem ctx o s = raise (ValidObjError(s,ctx,o)) + +let is_block mem o = match o with +| Ptr _ | Atm _ -> true +| Fun _ | Int _ -> false + +let is_int _mem o = match o with +| Int _ -> true +| Fun _ | Ptr _ | Atm _ -> false + +let is_int64 mem o = match o with +| Int _ | Fun _ | Atm _ -> false +| Ptr p -> + match LargeArray.get mem p with + | Int64 _ -> true + | Float64 _ | Struct _ | String _ -> false + +let is_float64 mem o = match o with +| Int _ | Fun _ | Atm _ -> false +| Ptr p -> + match LargeArray.get mem p with + | Float64 _ -> true + | Int64 _ | Struct _ | String _ -> false + +let get_int _mem = function +| Int i -> i +| Fun _ | Ptr _ | Atm _ -> assert false + +let tag mem o = match o with +| Atm tag -> tag +| Fun _ -> Obj.out_of_heap_tag +| Int _ -> Obj.int_tag +| Ptr p -> + match LargeArray.get mem p with + | Struct (tag, _) -> tag + | String _ -> Obj.string_tag + | Float64 _ -> Obj.double_tag + | Int64 _ -> Obj.custom_tag + +let size mem o = match o with +| Atm _ -> 0 +| Fun _ | Int _ -> assert false +| Ptr p -> + match LargeArray.get mem p with + | Struct (tag, blk) -> Array.length blk + | String _ | Float64 _ | Int64 _ -> assert false + +let field mem o i = match o with +| Atm _ | Fun _ | Int _ -> assert false +| Ptr p -> + match LargeArray.get mem p with + | Struct (tag, blk) -> Array.get blk i + | String _ | Float64 _ | Int64 _ -> assert false (* Check that object o is a block with tag t *) -let val_tag t ctx o = - if Obj.is_block o && Obj.tag o = t then () - else fail ctx o ("expected tag "^string_of_int t) - -let val_block ctx o = - if Obj.is_block o then - (if Obj.tag o > Obj.no_scan_tag then - fail ctx o "block: found no scan tag") - else fail ctx o "expected block obj" - -let val_dyn ctx o = - let fail () = fail ctx o "expected a Dyn.t" in - if not (Obj.is_block o) then fail () - else if not (Obj.size o = 2) then fail () - else if not (Obj.tag (Obj.field o 0) = Obj.int_tag) then fail () +let val_tag t mem ctx o = + if is_block mem o && tag mem o = t then () + else fail mem ctx o ("expected tag "^string_of_int t) + +let val_block mem ctx o = + if is_block mem o then + (if tag mem o > Obj.no_scan_tag then + fail mem ctx o "block: found no scan tag") + else fail mem ctx o "expected block obj" + +let val_dyn mem ctx o = + let fail () = fail mem ctx o "expected a Dyn.t" in + if not (is_block mem o) then fail () + else if not (size mem o = 2) then fail () + else if not (tag mem (field mem o 0) = Obj.int_tag) then fail () else () open Values -let rec val_gen v ctx o = match v with - | Tuple (name,vs) -> val_tuple ~name vs ctx o - | Sum (name,cc,vv) -> val_sum name cc vv ctx o - | Array v -> val_array v ctx o - | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] ctx o - | Opt v -> val_sum "option" 1 [|[|v|]|] ctx o - | Int -> if not (Obj.is_int o) then fail ctx o "expected an int" +let rec val_gen v mem ctx o = match v with + | Tuple (name,vs) -> val_tuple ~name vs mem ctx o + | Sum (name,cc,vv) -> val_sum name cc vv mem ctx o + | Array v -> val_array v mem ctx o + | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] mem ctx o + | Opt v -> val_sum "option" 1 [|[|v|]|] mem ctx o + | Int -> if not (is_int mem o) then fail mem ctx o "expected an int" | String -> - (try val_tag Obj.string_tag ctx o - with Failure _ -> fail ctx o "expected a string") + (try val_tag Obj.string_tag mem ctx o + with Failure _ -> fail mem ctx o "expected a string") | Any -> () - | Fail s -> fail ctx o ("unexpected object " ^ s) - | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o - | Dyn -> val_dyn ctx o - | Proxy { contents = v } -> val_gen v ctx o - | Uint63 -> val_uint63 ctx o - | Float64 -> val_float64 ctx o + | Fail s -> fail mem ctx o ("unexpected object " ^ s) + | Annot (s,v) -> val_gen v mem (ctx/CtxAnnot s) o + | Dyn -> val_dyn mem ctx o + | Proxy { contents = v } -> val_gen v mem ctx o + | Int64 -> val_int64 mem ctx o + | Float64 -> val_float64 mem ctx o (* Check that an object is a tuple (or a record). vs is an array of value representation for each field. Its size corresponds to the expected size of the object. *) -and val_tuple ?name vs ctx o = +and val_tuple ?name vs mem ctx o = let ctx = match name with | Some n -> ctx/CtxType n | _ -> ctx in let n = Array.length vs in let val_fld i v = - val_gen v (ctx/(CtxField i)) (Obj.field o i) in - val_block ctx o; - if Obj.size o = n then Array.iteri val_fld vs + val_gen v mem (ctx/(CtxField i)) (field mem o i) in + val_block mem ctx o; + if size mem o = n then Array.iteri val_fld vs else - fail ctx o - ("tuple size: found "^string_of_int (Obj.size o)^ + fail mem ctx o + ("tuple size: found "^string_of_int (size mem o)^ ", expected "^string_of_int n) (* Check that the object is either a constant constructor of tag < cc, @@ -113,35 +172,35 @@ and val_tuple ?name vs ctx o = The size of vv corresponds to the number of non-constant constructors, and the size of vv.(i) is the expected arity of the i-th non-constant constructor. *) -and val_sum name cc vv ctx o = +and val_sum name cc vv mem ctx o = let ctx = ctx/CtxType name in - if Obj.is_block o then - (val_block ctx o; + if is_block mem o then + (val_block mem ctx o; let n = Array.length vv in - let i = Obj.tag o in + let i = tag mem o in let ctx' = if n=1 then ctx else ctx/CtxTag i in - if i < n then val_tuple vv.(i) ctx' o - else fail ctx' o ("sum: unexpected tag")) - else if Obj.is_int o then - let (n:int) = Obj.magic o in + if i < n then val_tuple vv.(i) mem ctx' o + else fail mem ctx' o ("sum: unexpected tag")) + else if is_int mem o then + let (n:int) = get_int mem o in (if n<0 || n>=cc then - fail ctx o ("bad constant constructor "^string_of_int n)) - else fail ctx o "not a sum" + fail mem ctx o ("bad constant constructor "^string_of_int n)) + else fail mem ctx o "not a sum" (* Check the o is an array of values satisfying f. *) -and val_array v ctx o = - val_block (ctx/CtxType "array") o; - for i = 0 to Obj.size o - 1 do - val_gen v ctx (Obj.field o i) +and val_array v mem ctx o = + val_block mem (ctx/CtxType "array") o; + for i = 0 to size mem o - 1 do + val_gen v mem ctx (field mem o i) done -and val_uint63 ctx o = - if not (Uint63.is_uint63 o) then - fail ctx o "not a 63-bit unsigned integer" +and val_int64 mem ctx o = + if not (is_int64 mem o) then + fail mem ctx o "not a 63-bit unsigned integer" -and val_float64 ctx o = - if not (Float64.is_float64 o) then - fail ctx o "not a 64-bit float" +and val_float64 mem ctx o = + if not (is_float64 mem o) then + fail mem ctx o "not a 64-bit float" let print_frame = function | CtxType t -> t @@ -149,12 +208,11 @@ let print_frame = function | CtxField i -> Printf.sprintf "fld=%i" i | CtxTag i -> Printf.sprintf "tag=%i" i -let validate debug v x = - let o = Obj.repr x in - try val_gen v mt_ec o +let validate ~debug v (o, mem) = + try val_gen v mem mt_ec o with ValidObjError(msg,ctx,obj) -> (if debug then let ctx = List.rev_map print_frame ctx in print_endline ("Context: "^String.concat"/"ctx); - pr_obj obj); + pr_obj mem obj); failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")") diff --git a/checker/validate.mli b/checker/validate.mli index fbcea3121b..584ea6ed95 100644 --- a/checker/validate.mli +++ b/checker/validate.mli @@ -8,4 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val validate : bool -> Values.value -> 'a -> unit +open Analyze + +val validate : debug:bool -> Values.value -> data * obj LargeArray.t -> unit diff --git a/checker/values.ml b/checker/values.ml index 56321a27ff..fff166f27b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -34,7 +34,7 @@ type value = | Dyn | Proxy of value ref - | Uint63 + | Int64 | Float64 let fix (f : value -> value) : value = @@ -129,6 +129,9 @@ let v_cast = v_enum "cast_kind" 4 let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|] let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] +let v_uint63 = + if Sys.word_size == 64 then Int else Int64 + let rec v_constr = Sum ("constr",0,[| [|Int|]; (* Rel *) @@ -148,7 +151,7 @@ let rec v_constr = [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) - [|Uint63|]; (* Int *) + [|v_uint63|]; (* Int *) [|Float64|] (* Int *) |]) @@ -299,6 +302,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_univs; (* universes *) Opt (Array v_variance); + Opt (Array v_variance); Opt v_bool; v_typing_flags|] diff --git a/checker/values.mli b/checker/values.mli index ec3b91d5dd..15d307ee29 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -38,7 +38,7 @@ type value = | Proxy of value ref (** Same as the inner value, used to define recursive types *) - | Uint63 + | Int64 | Float64 (** NB: List and Opt have their own constructors to make it easy to diff --git a/checker/votour.ml b/checker/votour.ml index 9adcc874ac..452809f7bb 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -157,7 +157,7 @@ let rec get_name ?(extra=false) = function |Annot (s,v) -> s^"/"^get_name ~extra v |Dyn -> "<dynamic>" | Proxy v -> get_name ~extra !v - | Uint63 -> "Uint63" + | Int64 -> "Int64" | Float64 -> "Float64" (** For tuples, its quite handy to display the inner 1st string (if any). @@ -263,7 +263,7 @@ let rec get_children v o pos = match v with end |Fail s -> raise Forbidden | Proxy v -> get_children !v o pos - | Uint63 -> raise Exit + | Int64 -> raise Exit | Float64 -> raise Exit let get_children v o pos = diff --git a/clib/cUnix.ml b/clib/cUnix.ml index c5f6bebb8e..6e3ad59b1f 100644 --- a/clib/cUnix.ml +++ b/clib/cUnix.ml @@ -140,3 +140,20 @@ let same_file f1 = Unix.Unix_error _ -> false) with Unix.Unix_error _ -> (fun _ -> false) + +(* Copied from ocaml filename.ml *) +let prng = lazy(Random.State.make_self_init ()) + +let temp_file_name temp_dir prefix suffix = + let rnd = (Random.State.bits (Lazy.force prng)) land 0xFFFFFF in + Filename.concat temp_dir (Printf.sprintf "%s%06x%s" prefix rnd suffix) + +let mktemp_dir ?(temp_dir=Filename.get_temp_dir_name()) prefix suffix = + let rec try_name counter = + let name = temp_file_name temp_dir prefix suffix in + match Unix.mkdir name 0o700 with + | () -> name + | exception (Sys_error _ as e) -> + if counter >= 1000 then raise e else try_name (counter + 1) + in + try_name 0 diff --git a/clib/cUnix.mli b/clib/cUnix.mli index 17574b3c42..55d307c724 100644 --- a/clib/cUnix.mli +++ b/clib/cUnix.mli @@ -65,3 +65,5 @@ val waitpid_non_intr : int -> Unix.process_status (** Check if two file names refer to the same (existing) file *) val same_file : string -> string -> bool +(** Like [Stdlib.Filename.temp_file] but producing a directory. *) +val mktemp_dir : ?temp_dir:string -> string -> string -> string @@ -29,7 +29,6 @@ depends: [ build: [ [ "./configure" "-prefix" prefix "-native-compiler" "no" ] - [ "dune" "build" "@vodeps" ] - [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ] + [ "make" "-f" "Makefile.dune" "voboot" ] [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/default.nix b/default.nix index cfadca54d2..174e199014 100644 --- a/default.nix +++ b/default.nix @@ -42,7 +42,6 @@ stdenv.mkDerivation rec { buildInputs = [ hostname python3 time # coq-makefile timing tools - dune ] ++ (with ocamlPackages; [ ocaml findlib num ]) ++ optionals buildIde [ @@ -67,6 +66,7 @@ stdenv.mkDerivation rec { [ jq curl gitFull gnupg ] # Dependencies of the merging script ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ocamlformat ]) # Dev tools ++ [ graphviz ] # Useful for STM debugging + ++ [ dune_2 ] # Maybe the next build system ); src = @@ -111,7 +111,7 @@ stdenv.mkDerivation rec { setupHook = writeText "setupHook.sh" " addCoqPath () { if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then - export COQPATH=\"$COQPATH\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" + export COQPATH=\"\${COQPATH-}\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" fi } diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index c75acb0560..577ce35aae 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -420,6 +420,7 @@ copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOT ECHO ========== BUILD COQ ==========
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+RMDIR /S /Q "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87122e0fb5..9e9e3b4cfa 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -97,8 +97,11 @@ ######################################################################## # Coquelicot ######################################################################## -: "${coquelicot_CI_REF:=master}" -: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" +# Modified until https://gitlab.inria.fr/coquelicot/coquelicot/merge_requests/2 is merged +: "${coquelicot_CI_REF:=fix-rlist-import}" +: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/pedrot/coquelicot}" +# : "${coquelicot_CI_REF:=master}" +# : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" ######################################################################## @@ -209,7 +212,7 @@ ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=master}" +: "${bedrock2_CI_REF:=tested}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 2b1d2298f2..b9d6215e60 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -4,7 +4,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2 -data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) + +# "latest" is disabled due to lack of build credits upstream, thus artifacts fail +# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) +data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index a9cc91170f..f08a08531f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; }) let unicoq = callPackage ./unicoq { inherit coq; }; in +let StructTact = coqPackages.StructTact.overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master"; + }); in + +let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master"; + }); in + +let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/verdi/tarball/master"; + }); in + let callPackage = newScope { inherit coq bignums coq-ext-lib coqprime corn iris math-classes - mathcomp simple-io ssreflect stdpp unicoq; + mathcomp simple-io ssreflect stdpp unicoq Verdi; }; in # Environments for building CI libraries with this Coq @@ -89,6 +103,7 @@ let projects = { mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; quickchick = callPackage ./quickchick.nix {}; + verdi-raft = callPackage ./verdi-raft.nix {}; VST = callPackage ./VST.nix {}; }; in diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 0f0ee91387..1105fba7a6 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ -{ coqprime }: +{ ocamlPackages }: { - coqBuildInputs = [ coqprime ]; + buildInputs = with ocamlPackages; [ ocaml findlib ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; - make = "make new-pipeline c-files"; + make = "make c-files printlite lite && make -j 1 coq"; } diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix new file mode 100644 index 0000000000..6a98f4ef47 --- /dev/null +++ b/dev/ci/nix/verdi-raft.nix @@ -0,0 +1,5 @@ +{ Verdi }: +{ + coqBuildInputs = [ Verdi ]; + configure = "./configure"; +} diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh new file mode 100644 index 0000000000..a125337dd9 --- /dev/null +++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh @@ -0,0 +1,33 @@ +if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then + + mathcomp_CI_REF=non_maximal_implicit + mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp + + oddorder_CI_REF=non_maximal_implicit + oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order + + stdlib2_CI_REF=non_maximal_implicit + stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2 + + coq_dpdgraph_CI_REF=non_maximal_implicit + coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph + + vst_CI_REF=non_maximal_implicit + vst_CI_GITURL=https://github.com/SimonBoulier/VST + + equations_CI_REF=non_maximal_implicit + equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations + + mtac2_CI_REF=non_maximal_implicit + mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2 + + relation_algebra_CI_REF=non_maximal_implicit + relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra + + fiat_parsers_CI_REF=non_maximal_implicit + fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat + + Corn_CI_REF=non_maximal_implicit + Corn_CI_GITURL=https://github.com/SimonBoulier/corn + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 37c6e2f619..cd35064b18 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,24 +108,44 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec -- dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg coqc foo.v (ocd) source dune_db ``` -or +to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`: ``` -dune exec -- dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker foo.vo (ocd) source dune_db ``` -for the checker. Unfortunately, dependency handling here is not fully -refined, so you need to build enough of Coq once to use this target -[it will then correctly compute the deps and rebuild if you call the -script again] This will be fixed in the future. +Unfortunately, dependency handling here is not fully refined, so you +need to build enough of Coq once to use this target [it will then +correctly compute the deps and rebuild if you call the script again] +This will be fixed in the future. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. +**Note**: If you are using OCaml >= 4.08 you need to use + +``` +(ocd) source dune_db_408 +``` + +or + +``` +(ocd) source dune_db_409 +``` + +depending on your OCaml version. This is due to several factors: + +- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source` + is not re entrant and seems to doubly-load in the default setup, see + https://github.com/coq/coq/issues/8952 +- OCaml >= 4.09 comes with `dynlink` already linked in so we need to + modify the list of modules loaded. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 2d187f7bae..3260040248 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -158,7 +158,7 @@ Universes component: universe polymorphism, asynchronous proofs summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one - impacted released: V8.5-V8.10 + impacted released versions: V8.5-V8.10 impacted development branches: none impacted coqchk versions: immune fixed in: PR#10664 @@ -167,6 +167,19 @@ Universes GH issue number: none risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + component: algebraic universes + summary: Set+2 was incorrectly simplified to Set+1 + introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a) + impacted released versions: V8.10.0 V8.10.1 V8.10.2 + impacted coqchk versions: same + fixed in: PR#11422 + found by: Gilbert + exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration) + GH issue number: see PR + risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic + universes such that +2 increments do not appear), mild risk from plugins which manipulate + algebraic universes. + Primitive projections component: primitive projections, guard condition diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 1c486b024d..ba68501e04 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -75,7 +75,8 @@ in time. - [ ] Pin the versions of libraries and plugins in `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it exists, a branch dedicated to compatibility with the corresponding - Coq branch). + Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this + semi-automatically. - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The project should have a "Request X.X+beta1 inclusion" column for the PRs that were diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 0fc0a413ba..fca7b77fc2 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -1,12 +1,11 @@ # Coq XML Protocol This document is based on documentation originally written by CJ Bell -for his [vscoq](https://github.com/siegebell/vscoq/) project. +for his [vscoq](https://github.com/coq-community/vscoq/) project. Here, the aim is to provide a "hands on" description of the XML protocol that coqtop and IDEs use to communicate. The protocol first appeared -with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming -versions of Proof General. +with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). @@ -13,6 +13,8 @@ ../checker/coqchk.bc ../topbin/coqc_bin.bc ../ide/coqide_main.bc - ; This is not enough as the call to `ocamlfind` will fail :/ + %{lib:coq.plugins.ltac:ltac_plugin.cma} + ; This is not enough, the call to `ocamlfind` may fail if the + ; META file is not yet in place :/ top_printers.cma) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 1382f4d1b6..498f167eb1 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -7,11 +7,21 @@ case $1 in exe=_build/default/checker/coqchk.bc ;; coqide) + shift exe=_build/default/ide/coqide_main.bc ;; - *) + coqc) + shift exe=_build/default/topbin/coqc_bin.bc ;; + coqtop) + shift + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; + *) + echo "First argument must be one of {coqc,coqtop,checker,coqide}" + exit 1 + ;; esac emacs="${INSIDE_EMACS:+-emacs}" diff --git a/dev/dune_db_408 b/dev/dune_db_408 new file mode 100644 index 0000000000..3bf13da62d --- /dev/null +++ b/dev/dune_db_408 @@ -0,0 +1,25 @@ +load_printer threads.cma +load_printer str.cma +load_printer config.cma +load_printer clib.cma +load_printer dynlink.cma +load_printer lib.cma +load_printer gramlib.cma +load_printer byterun.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +load_printer proofs.cma +load_printer parsing.cma +load_printer printing.cma +load_printer tactics.cma +load_printer vernac.cma +load_printer stm.cma +load_printer toplevel.cma + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/dune_db_409 b/dev/dune_db_409 new file mode 100644 index 0000000000..1267fd5393 --- /dev/null +++ b/dev/dune_db_409 @@ -0,0 +1,24 @@ +load_printer threads.cma +load_printer str.cma +load_printer config.cma +load_printer clib.cma +load_printer lib.cma +load_printer gramlib.cma +load_printer byterun.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +load_printer proofs.cma +load_printer parsing.cma +load_printer printing.cma +load_printer tactics.cma +load_printer vernac.cma +load_printer stm.cma +load_printer toplevel.cma + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 224601bbce..553696410c 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -33,6 +33,6 @@ echo Checking overlays dev/tools/check-overlays.sh || CODE=1 echo Checking ocamlformat -dune build @fmt || CODE=1 +make -f Makefile.dune fmt || CODE=1 exit $CODE diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 677377f868..54baaee1fe 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz"; - sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq"; + url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz"; + sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"; }) diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c0a3eeb11c..a888998ebf 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -137,7 +137,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then else error "Local branch is not up-to-date with ${REMOTE}." error "Pull before merging." - ask_confirmation + # This check should never be bypassed. + exit 1 fi fi diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh new file mode 100755 index 0000000000..dbf54d7f0a --- /dev/null +++ b/dev/tools/pin-ci.sh @@ -0,0 +1,46 @@ +#!/usr/bin/env bash + +# Use this script to pin the commit used by the developments tracked by the CI + +OVERLAYS="./dev/ci/ci-basic-overlay.sh" + +process_development() { + local DEV=$1 + local REPO_VAR="${DEV}_CI_GITURL" + local REPO=${!REPO_VAR} + local BRANCH_VAR="${DEV}_CI_REF" + local BRANCH=${!BRANCH_VAR} + if [[ -z "$BRANCH" ]] + then + echo "$DEV has no branch set, skipping" + return 0 + fi + if [[ $BRANCH =~ ^[a-f0-9]{40}$ ]] + then + echo "$DEV is already set to hash $BRANCH, skipping" + return 0 + fi + echo "Resolving $DEV as $BRANCH from $REPO" + local HASH=$(git ls-remote --heads $REPO $BRANCH | cut -f 1) + if [[ -z "$HASH" ]] + then + echo "Could not resolve reference $BRANCH for $DEV (something went wrong), skipping" + return 0 + fi + read -p "Expand $DEV from $BRANCH to $HASH? [y/N] " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]]; then + # use -i.bak to be compatible with MacOS; see, e.g., https://stackoverflow.com/a/7573438/377022 + sed -i.bak -e "s/$BRANCH_VAR:=$BRANCH/$BRANCH_VAR:=$HASH/" $OVERLAYS + fi +} + +# Execute the script to set the overlay variables +. $OVERLAYS + +# Find all variables declared in the base overlay of the form *_CI_GITURL +for REPO_VAR in $(compgen -A variable | grep _CI_GITURL) +do + DEV=${REPO_VAR%_CI_GITURL} + process_development $DEV +done diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst deleted file mode 100644 index 8c84648aa7..0000000000 --- a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** `#11360 <https://github.com/issues/11360>`_ - Broken section closing when a template polymorphic inductive type depends on - a section variable through its parameters (`#11361 - <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst deleted file mode 100644 index 8983e162fb..0000000000 --- a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Changed heuristics for universe minimization to :g:`Set`: only - minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, - by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst deleted file mode 100644 index 941469d698..0000000000 --- a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - A dependency was missing when looking for default clauses in the - algorithm for printing pattern matching clauses (`#11233 - <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing - `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry - Jay). diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst new file mode 100644 index 0000000000..a7ffde31fc --- /dev/null +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -0,0 +1,6 @@ +- **Changed:** + The warning raised when a trailing implicit is declared to be non maximally + inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error. + This was deprecated since Coq 8.10. + (`#11368 <https://github.com/coq/coq/pull/11368>`_, + by SimonBoulier). diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst deleted file mode 100644 index a1b8594f5f..0000000000 --- a/doc/changelog/03-notations/11276-master+fix10750.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - :cmd:`Print Visibility` was failing in the presence of only-printing notations - (`#11276 <https://github.com/coq/coq/pull/11276>`_, - by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst deleted file mode 100644 index ae9888512d..0000000000 --- a/doc/changelog/03-notations/11311-custom-entries-recursive.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Recursive notations with custom entries were incorrectly parsing `constr` - instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ - by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, - `#9490 <https://github.com/coq/coq/pull/9490>`_). diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst deleted file mode 100644 index 2fef75dc7f..0000000000 --- a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The tactics :tacn:`eapply`, :tacn:`refine` and its variants no - longer allows shelved goals to be solved by typeclass resolution. - (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst deleted file mode 100644 index cdfd2b228e..0000000000 --- a/doc/changelog/04-tactics/11203-fix-time-printing.rst +++ /dev/null @@ -1,4 +0,0 @@ -- The optional string argument to :tacn:`time` is now properly quoted - under :cmd:`Print Ltac` (`#11203 - <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 - <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst deleted file mode 100644 index ebfb6c19b1..0000000000 --- a/doc/changelog/04-tactics/11263-micromega-fix.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed** - Efficiency regression introduced by PR `#9725 <https://github.com/coq/coq/pull/9725>`_. - (`#11263 <https://github.com/coq/coq/pull/11263>`_, - fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, - and `#11242 <https://github.com/coq/coq/issues/11242>`_, - and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst deleted file mode 100644 index 25e929e030..0000000000 --- a/doc/changelog/04-tactics/11337-omega-with-depr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - The undocumented ``omega with`` tactic variant has been deprecated, - using ``lia`` is the recommended replacement, tho the old semantics - of ``omega with *`` can be recovered with ``zify; omega`` - (`#11337 <https://github.com/coq/coq/pull/11337>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst new file mode 100644 index 0000000000..5ecd46bced --- /dev/null +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Regression of ``lia`` due to more powerful ``zify`` + (`#11362 <https://github.com/coq/coq/pull/11362>`_, + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, + by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst new file mode 100644 index 0000000000..4eb2732106 --- /dev/null +++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml. + (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst deleted file mode 100644 index 462ba4a7b1..0000000000 --- a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. - (`#11241 <https://github.com/coq/coq/pull/11241>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst new file mode 100644 index 0000000000..b9ecd140e7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -0,0 +1 @@ +- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst deleted file mode 100644 index ecc134748d..0000000000 --- a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coqtop --version`` was broken when called in the middle of an installation process - (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing - `#11254 <https://github.com/coq/coq/pull/11254>`_). diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst deleted file mode 100644 index 599db5b1da..0000000000 --- a/doc/changelog/08-tools/11357-master.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable - together with an unpacked (``mllib``) plugin. (`#11357 - <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst deleted file mode 100644 index 5c08e2b0ea..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` - environment variable - (`#11227 <https://github.com/coq/coq/pull/11227>`_, - by Bernhard M. Wiedemann). diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst new file mode 100644 index 0000000000..c6778403d4 --- /dev/null +++ b/doc/changelog/12-misc/10486-native-string-extraction.rst @@ -0,0 +1,7 @@ +- **Added:** + Support for better extraction of strings in OCaml and Haskell: + `ExtOcamlNativeString` provides bindings from the Coq `String` type to + the OCaml `string` type, and string literals can be extracted to literals, + both in OCaml and Haskell. (`#10486 + <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from + Maxime Dénès, review by Hugo Herbelin). diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 7136cc28d1..d909f98956 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of the |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] +.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first :token:`string`) and all its - constructors (all the :token:`string` between square brackets). In this form, + extractions for the type itself (:n:`@string__1`) and all its + constructors (all the :n:`@string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. + When :n:`@string__1` matches the name of the type of characters or strings + (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String`` + for Haskell), extraction of literals is handled in a specialized way, so as + to generate literals in the target language. This feature requires the type + designated by :n:`@qualid` to be registered as the standard char or string type, + using the :cmd:`Register` command. + .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra :token:`string` that indicates how to diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 650a444a16..daca43e65e 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -5,6 +5,27 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic :Author: Pierre Crégut +.. warning:: + + The :tacn:`omega` tactic is about to be deprecated in favor of the + :tacn:`lia` tactic. The goal is to consolidate the arithmetic + solving capabilities of Coq into a single engine; moreover, + :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a + complete Presburger arithmetic solver while :tacn:`omega` was known + to be incomplete). + + Work is in progress to make sure that there are no regressions + (including no performance regression) when switching from + :tacn:`omega` to :tacn:`lia` in existing projects. However, we + already recommend using :tacn:`lia` in new or refactored proof + scripts. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, + especially if the issue was not present in :tacn:`omega`. + + Note that replacing :tacn:`omega` with :tacn:`lia` can break + non-robust proof scripts which rely on incompleteness bugs of + :tacn:`omega` (e.g. using the pattern :g:`; try omega`). + Description of ``omega`` ------------------------ diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 35729d852d..7a50748c51 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with Batch mode --------------- + .. warning:: + + The ``-vio`` flag is subsumed, for most practical usage, by the + the more recent ``-vos`` flag. See :ref:`compiled-interfaces`. + + .. warning:: + + When working with ``.vio`` files, do not use the ``-vos`` option at + the same time, otherwise stale files might get loaded when executing + a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is + assigned higher priority than the loading of a ``.vio`` file. + When |Coq| is used as a batch compiler by running ``coqc``, it produces a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other things, theorem statements and proofs. Hence to produce a .vo |Coq| @@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file. The asynchronous processing of proofs can decouple the generation of a compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the -generation and checking of the proof objects. The ``-quick`` flag can be +generation and checking of the proof objects. The ``-vio`` flag can be passed to ``coqc`` to produce, quickly, ``.vio`` files. Alternatively, when using a Makefile produced by ``coq_makefile``, -the ``quick`` target can be used to compile all files using the ``-quick`` flag. +the ``vio`` target can be used to compile all files using the ``-vio`` flag. A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but proofs will not be available (the Print command produces an error). @@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof objects, but proof tasks, i.e. what a worker process can transform into a proof object. -Compiling a set of files with the ``-quick`` flag allows one to work, +Compiling a set of files with the ``-vio`` flag allows one to work, interactively, on any file without waiting for all the proofs to be checked. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7adb25cbd6..f9cc25959c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -529,8 +529,8 @@ sections, except in the following ways: Polymorphic Universe i. Fail Constraint i = i. - This includes constraints implictly declared by commands such as - :cmd:`Variable`, which may as a such need to be used with universe + This includes constraints implicitly declared by commands such as + :cmd:`Variable`, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): .. coqtop:: all diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 33fc211fa5..6d9979a704 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -50,23 +50,28 @@ __ 811RefineInstance_ __ 811SSRUnderOver_ __ 811Reals_ -The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| -and affected releases. See the `Changes in 8.11+beta1`_ section for the -detailed list of changes, including potentially breaking changes marked with -**Changed**. +Additionally, while the :tacn:`omega` tactic is not yet deprecated in +this version of Coq, it should soon be the case and we already +recommend users to switch to :tacn:`lia` in new proof scripts (see +also the warning message in the :ref:`corresponding chapter <omega>`). + +The ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ +section and following sections for the detailed list of changes, +including potentially breaking changes marked with **Changed**. + +Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of +the ML API), https://coq.github.io/doc/v8.11/refman (reference +manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of +the standard library). Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the +Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of -the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference -manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of -the standard library). - The OPAM repository for |Coq| packages has been maintained by -Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions -from many users. A list of packages is available at +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with +contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. The 61 contributors to this version are Michael D. Adams, Guillaume @@ -509,6 +514,133 @@ Changes in 8.11+beta1 (`#10471 <https://github.com/coq/coq/pull/10471>`_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). +- **Fixed:** `#11360 <https://github.com/issues/11360>`_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). +- **Fixed:** The type of :g:`Set+1` would be computed to be itself, + leading to a proof of False (`#11422 + <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, + by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing + `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 <https://github.com/coq/coq/pull/11276>`_, + by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ + by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, + `#9490 <https://github.com/coq/coq/pull/9490>`_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) +- **Fixed:** + Efficiency regression of :tacn:`lia` introduced in 8.10 + by PR `#9725 <https://github.com/coq/coq/pull/9725>`_ + (`#11263 <https://github.com/coq/coq/pull/11263>`_, + fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, + and `#11242 <https://github.com/coq/coq/issues/11242>`_, + and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated. + Using :tacn:`lia` is the recommended replacement, though the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 <https://github.com/coq/coq/pull/11337>`_, + by Emilio Jesus Gallego Arias). +- **Fixed** + For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. + It can be enabled by explicitly loading the module :g:`ZifyPow` + (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 + (`#11241 <https://github.com/coq/coq/pull/11241>`_, + by Hugo Herbelin). + +**Commands and options** + +- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command + line options have been deprecated; their use was very limited, you + can achieve the same by adding object files in the linking step or + by using a plugin (`#11428 + <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego + Arias). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). +- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for + consistency with the new ``-vos`` and ``-vok`` flags. Usage of + ``-quick`` is now deprecated (`#11280 + <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin (`#11357 + <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). + +**CoqIDE** + +- **Changed:** CoqIDE now uses the GtkSourceView native implementation + of the autocomplete mechanism (`#11400 + <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot). + +**Standard library** + +- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and + :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be + imported explicitly where required (`#11396 + <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overridden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index e746096df2..510e271951 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1728,11 +1728,11 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. warn:: Argument number @num is a trailing implicit so must be maximal. +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance in - .. coqtop:: all warn + .. coqtop:: all fail Arguments prod _ [_]. @@ -1983,6 +1983,8 @@ Deactivation of implicit arguments for parsing to be given as if no arguments were implicit. By symmetry, this also affects printing. +.. _canonical-structure-declaration: + Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -1993,6 +1995,7 @@ value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid + :name: Canonical Structure This command declares :token:`qualid` as a canonical instance of a structure (a record). When the :g:`#[local]` attribute is given the effect diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 70dadedd35..d591718b17 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1620,6 +1620,17 @@ variety of commands: :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, :n:`@string__3` is the note. +``canonical`` + This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. + It is equivalent to having a :cmd:`Canonical Structure` declaration just + after the command. + + This attirbute can take the value ``false`` when decorating a record field + declaration with the effect of preventing the field from being involved in + the inference of canonical instances. + + See also :ref:`canonical-structure-declaration`. + .. example:: .. coqtop:: all reset warn diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d4a61425e1..ba43128bdc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -253,6 +253,7 @@ and ``coqtop``, unless stated otherwise: :-h, --help: Print a short usage and exit. +.. _compiled-interfaces: Compiled interfaces (produced using ``-vos``) ---------------------------------------------- diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index dd80b29bda..b722b1af74 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -940,6 +940,13 @@ below will fail immediately and won't print anything. In any case, the value returned by the fully applied quotation is an unspecified dummy Ltac1 closure and should not be further used. +Switching between Ltac languages +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We recommend using the :opt:`Default Proof Mode` option to switch between tactic +languages with a proof-based granularity. This allows to incrementally port +the proof scripts. + Transition from Ltac1 --------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 6884b6e998..b1734b3f19 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -265,6 +265,35 @@ Name a set of section hypotheses for ``Proof using`` has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. +Proof modes +``````````` + +When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, +|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard |Coq| installation, and furthermore some plugins define +their own proof modes. The default proof mode used when opening a proof can +be changed using the following option. + +.. opt:: Default Proof Mode @string + :name: Default Proof Mode + + Select the proof mode to use when starting a proof. Depending on the proof + mode, various syntactic constructs are allowed when writing an interactive + proof. The possible option values are listed below. + + - "Classic": this is the default. It activates the |Ltac| language to interact + with the proof, and also allows vernacular commands. + + - "Noedit": this proof mode only allows vernacular commands. No tactic + language is activated at all. This is the default when the prelude is not + loaded, e.g. through the `-noinit` option for `coqc`. + + - "Ltac2": this proof mode is made available when requiring the Ltac2 + library, and is set to be the default when it is imported. It allows + to use the Ltac2 language, as well as vernacular commands. + + - Some external plugins also define their own proof mode, which can be + activated via this command. Navigation in the proof tree -------------------------------- @@ -490,6 +519,13 @@ The following example script illustrates all these features: You just finished a goal focused by ``{``, you must unfocus it with ``}``. +Mandatory Bullets +````````````````` + +Using :opt:`Default Goal Selector` with the ``!`` selector forces +tactic scripts to keep focus to exactly one goal (e.g. using bullets) +or use explicit goal selectors. + Set Bullet Behavior ``````````````````` .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 89b24ea8a3..a38c26c2b3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,7 +1200,7 @@ Controlling the locality of commands + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier + when no section contains them. For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 7fe2493fbf..828caecabc 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,8 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins)) + (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} ; On windows run will fail @@ -17,6 +18,7 @@ ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. @@ -24,7 +26,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b816ef6210..dbc3a42ee9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,12 +12,14 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlChar.v plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOCamlFloats.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlNativeString.v plugins/extraction/ExtrOcamlZBigInt.v plugins/extraction/ExtrOcamlZInt.v plugins/extraction/Extraction.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index ac611926b3..5e13214a1a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p> plugins/ssr/ssrfun.v </dd> + <dt> <b>Ltac2</b>: + The Ltac2 tactic programming language + </dt> + <dd> + user-contrib/Ltac2/Ltac2.v + user-contrib/Ltac2/Array.v + user-contrib/Ltac2/Bool.v + user-contrib/Ltac2/Char.v + user-contrib/Ltac2/Constr.v + user-contrib/Ltac2/Control.v + user-contrib/Ltac2/Env.v + user-contrib/Ltac2/Fresh.v + user-contrib/Ltac2/Ident.v + user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Int.v + user-contrib/Ltac2/List.v + user-contrib/Ltac2/Ltac1.v + user-contrib/Ltac2/Message.v + user-contrib/Ltac2/Notations.v + user-contrib/Ltac2/Option.v + user-contrib/Ltac2/Pattern.v + user-contrib/Ltac2/Std.v + user-contrib/Ltac2/String.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index bea6f24098..732f15b78a 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash # Instantiate links to library files in index template @@ -8,9 +8,14 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do + if [[ $k =~ "user-contrib" ]]; then + BASE_PREFIX="" + else + BASE_PREFIX="Coq." + fi d=`basename $k` ls $k | grep -q \.v'$' if [ $? = 0 ]; then @@ -26,7 +31,7 @@ for k in $LIBDIRS; do echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` - sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else diff --git a/ide/coqide.ml b/ide/coqide.ml index fc30690544..918c196968 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -618,7 +618,7 @@ let printopts_callback opts v = let get_current_word term = (* First look to find if autocompleting *) - match term.script#complete_popup#proposal with + match term.script#proposal with | Some p -> p | None -> (* Then look at the current selected word *) diff --git a/ide/preferences.ml b/ide/preferences.ml index 4ee5669877..d3cf08e90e 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -388,6 +388,9 @@ let window_height = let auto_complete = new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool) +let auto_complete_delay = + new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int) + let stop_before = new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool) @@ -831,10 +834,26 @@ let configure ?(apply=(fun () -> ())) parent = let but = GButton.check_button ~label:text ~active ~packing:box#pack () in ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active)) in + let spin text ~min ~max (pref : int preference) = + let box = GPack.hbox ~packing:box#pack () in + let but = GEdit.spin_button + ~numeric:true ~update_policy:`IF_VALID ~digits:0 + ~packing:box#pack () + in + let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in + let () = but#adjustment#set_bounds + ~lower:(float_of_int min) ~upper:(float_of_int max) + ~step_incr:1. + () + in + let () = but#set_value (float_of_int pref#get) in + ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int)) + in let () = button "Dynamic word wrap" dynamic_word_wrap in let () = button "Show line number" show_line_number in let () = button "Auto indentation" auto_indent in let () = button "Auto completion" auto_complete in + let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in let () = button "Show spaces" show_spaces in let () = button "Show right margin" show_right_margin in let () = button "Show progress bar" show_progress_bar in diff --git a/ide/preferences.mli b/ide/preferences.mli index 4b04326cec..7b43079b4f 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -82,6 +82,7 @@ val show_toolbar : bool preference val window_width : int preference val window_height : int preference val auto_complete : bool preference +val auto_complete_delay : int preference val stop_before : bool preference val reset_on_tab_switch : bool preference val line_ending : line_ending preference diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index ac6712909e..396939cfcc 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -69,387 +69,101 @@ let is_substring s1 s2 = if !break then len2 - len1 else -1 -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -let complete_model_signals - (start_s : int GUtil.signal) - (update_s : (int * string * Proposals.t) GUtil.signal) - (end_s : unit GUtil.signal) : complete_model_signals = -let signals = [ - start_s#disconnect; - update_s#disconnect; - end_s#disconnect; -] in -object (self : 'a) - inherit GUtil.ml_signals signals - method start_completion = start_s#connect ~after - method update_completion = update_s#connect ~after - method end_completion = end_s#connect ~after -end - -class complete_model coqtop (buffer : GText.buffer) = - let cols = new GTree.column_list in - let column = cols#add Gobject.Data.string in - let store = GTree.list_store cols in - let filtered_store = GTree.model_filter store in - let start_completion_signal = new GUtil.signal () in - let update_completion_signal = new GUtil.signal () in - let end_completion_signal = new GUtil.signal () in -object (self) - - val signals = complete_model_signals - start_completion_signal update_completion_signal end_completion_signal - val mutable active = false - val mutable auto_complete_length = 3 - (* this variable prevents CoqIDE from autocompleting when we have deleted something *) - val mutable is_auto_completing = false - (* this mutex ensure that CoqIDE will not try to autocomplete twice *) - val mutable cache = (-1, "", Proposals.empty) - val mutable insert_offset = -1 - val mutable current_completion = ("", Proposals.empty) - val mutable lock_auto_completing = true +class completion_provider coqtop = + let self_provider = ref None in + let active = ref true in + let provider = object (self) - method connect = signals + val mutable auto_complete_length = 3 + val mutable cache = (-1, "", Proposals.empty) + val mutable insert_offset = -1 - method active = active + method name = "" - method set_active b = active <- b + method icon = None - method private handle_insert iter s = - (* we're inserting, so we may autocomplete *) - is_auto_completing <- true + method private update_proposals pref = + let (_, _, props) = cache in + let filter prop = 0 <= is_substring pref prop in + let props = Proposals.filter filter props in + props - method private handle_delete ~start ~stop = - (* disable autocomplete *) - is_auto_completing <- false - - method store = filtered_store - - method column = column - - method handle_proposal path = - let row = filtered_store#get_iter path in - let proposal = filtered_store#get ~row ~column in - let (start_offset, _, _) = cache in - (* [iter] might be invalid now, get a new one to please gtk *) - let iter = buffer#get_iter `INSERT in - (* We cancel completion when the buffer has changed recently *) - if iter#offset = insert_offset then begin - let suffix = - let len1 = String.length proposal in - let len2 = insert_offset - start_offset in - String.sub proposal len2 (len1 - len2) + method private add_proposals ctx props = + let mk text = + let item = GSourceView3.source_completion_item ~text ~label:text () in + (item :> GSourceView3.source_completion_proposal) in - buffer#begin_user_action (); - ignore (buffer#insert_interactive ~iter suffix); - buffer#end_user_action (); - end - - method private init_proposals pref props = - let () = store#clear () in - let iter prop = - let iter = store#append () in - store#set ~row:iter ~column prop - in - let () = current_completion <- (pref, props) in - Proposals.iter iter props - - method private update_proposals pref = - let (_, _, props) = cache in - let filter prop = 0 <= is_substring pref prop in - let props = Proposals.filter filter props in - let () = current_completion <- (pref, props) in - let () = filtered_store#refilter () in - props - - method private do_auto_complete k = - let iter = buffer#get_iter `INSERT in - let () = insert_offset <- iter#offset in - let log = Printf.sprintf "Completion at offset: %i" insert_offset in - let () = Minilib.log log in - let prefix = - if Gtk_parsing.ends_word iter then - let start = Gtk_parsing.find_word_start iter in - let w = buffer#get_text ~start ~stop:iter () in - if String.length w >= auto_complete_length then Some (w, start) - else None - else None - in - match prefix with - | Some (w, start) -> + let props = List.map mk (Proposals.elements props) in + ctx#add_proposals (Option.get !self_provider) props true + + method populate ctx = + let iter = ctx#iter in + let buffer = new GText.buffer iter#buffer in + let start = Gtk_parsing.find_word_start iter in + let w = start#get_text ~stop:iter in let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in let (off, prefix, props) = cache in let start_offset = start#offset in (* check whether we have the last request in cache *) if (start_offset = off) && (0 <= is_substring prefix w) then let props = self#update_proposals w in - let () = update_completion_signal#call (start_offset, w, props) in - k () + self#add_proposals ctx props else - let () = start_completion_signal#call start_offset in + let cancel = ref false in + let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in let update props = let () = cache <- (start_offset, w, props) in - let () = self#init_proposals w props in - update_completion_signal#call (start_offset, w, props) + if not !cancel then self#add_proposals ctx props in (* If not in the cache, we recompute it: first syntactic *) let synt = get_syntactic_completion buffer w Proposals.empty in (* Then semantic *) - let next prop = - let () = update prop in - Coq.lift k + let next props = + update props; + Coq.return () in let query = Coq.bind (get_semantic_completion w synt) next in (* If coqtop is computing, do the syntactic completion altogether *) - let occupied () = - let () = update synt in - k () - in + let occupied () = update synt in Coq.try_grab coqtop query occupied - | None -> end_completion_signal#call (); k () - - method private may_auto_complete () = - if active && is_auto_completing && lock_auto_completing then begin - let () = lock_auto_completing <- false in - let unlock () = lock_auto_completing <- true in - self#do_auto_complete unlock - end - - initializer - let filter_prop model row = - let (_, props) = current_completion in - let prop = store#get ~row ~column in - Proposals.mem prop props - in - let () = filtered_store#set_visible_func filter_prop in - (* Install auto-completion *) - ignore (buffer#connect#insert_text ~callback:self#handle_insert); - ignore (buffer#connect#delete_range ~callback:self#handle_delete); - ignore (buffer#connect#after#end_user_action ~callback:self#may_auto_complete); - -end - -class complete_popup (model : complete_model) (view : GText.view) = - let obj = GWindow.window ~kind:`POPUP ~show:false () in - let frame = GBin.scrolled_window - ~hpolicy:`NEVER ~vpolicy:`NEVER - ~shadow_type:`OUT ~packing:obj#add () - in -(* let frame = GBin.frame ~shadow_type:`OUT ~packing:obj#add () in *) - let data = GTree.view - ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment - ~rules_hint:true ~headers_visible:false - ~model:model#store ~packing:frame#add () - in - let renderer = GTree.cell_renderer_text [], ["text", model#column] in - let col = GTree.view_column ~renderer () in - let _ = data#append_column col in - let () = col#set_sizing `AUTOSIZE in - let page_size = 16 in - -object (self) - - method coerce = view#coerce - - method private refresh_style () = - let (renderer, _) = renderer in - let font = Pango.Font.from_string Preferences.text_font#get in - renderer#set_properties [`FONT_DESC font; `XPAD 10] - - method private coordinates pos = - (* Toplevel position w.r.t. screen *) - let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in - (* Position of view w.r.t. window *) - let (ux, uy) = Gdk.Window.get_position view#misc#window in - (* Relative buffer position to view *) - let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in - (* Iter position *) - let iter = view#buffer#get_iter pos in - let coords = view#get_iter_location iter in - let lx = Gdk.Rectangle.x coords in - let ly = Gdk.Rectangle.y coords in - let w = Gdk.Rectangle.width coords in - let h = Gdk.Rectangle.height coords in - (* Absolute position *) - (x + lx + ux - dx, y + ly + uy - dy, w, h) - - method private select_any f = - let sel = data#selection#get_selected_rows in - let path = match sel with - | [] -> - begin match model#store#get_iter_first with - | None -> None - | Some iter -> Some (model#store#get_path iter) - end - | path :: _ -> Some path - in - match path with - | None -> () - | Some path -> - let path = f path in - let _ = data#selection#select_path path in - data#scroll_to_cell ~align:(0.,0.) path col - - method private select_previous () = - let prev path = - let copy = GTree.Path.copy path in - if GTree.Path.prev path then path - else copy - in - self#select_any prev - - method private select_next () = - let next path = - let () = GTree.Path.next path in - path - in - self#select_any next - method private select_previous_page () = - let rec up i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up (pred i) path - else copy - in - self#select_any (up page_size) + method matched ctx = + if !active then + let iter = ctx#iter in + let () = insert_offset <- iter#offset in + let log = Printf.sprintf "Completion at offset: %i" insert_offset in + let () = Minilib.log log in + if Gtk_parsing.ends_word iter#backward_char then + let start = Gtk_parsing.find_word_start iter in + iter#offset - start#offset >= auto_complete_length + else false + else false - method private select_next_page () = - let rec down i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (pred i) (model#store#get_path iter) - else copy - in - self#select_any (down page_size) + method activation = [`INTERACTIVE; `USER_REQUESTED] - method private select_first () = - let rec up path = - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up path - else copy - in - self#select_any up + method info_widget proposal = None - method private select_last () = - let rec down path = - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (model#store#get_path iter) - else copy - in - self#select_any down + method update_info proposal info = () - method private select_enter () = - let sel = data#selection#get_selected_rows in - match sel with - | [] -> () - | path :: _ -> - let () = model#handle_proposal path in - self#hide () + method start_iter ctx proposal iter = false - method proposal = - let sel = data#selection#get_selected_rows in - if obj#misc#visible then match sel with - | [] -> None - | path :: _ -> - let row = model#store#get_iter path in - let column = model#column in - let proposal = model#store#get ~row ~column in - Some proposal - else None + method activate_proposal proposal iter = false - method private manage_scrollbar () = - (* HACK: we don't have access to the treeview size because of the lack of - LablGTK binding for certain functions, so we bypass it by approximating - it through the size of the proposals *) - let height = match model#store#get_iter_first with - | None -> -1 - | Some iter -> - let path = model#store#get_path iter in - let area = data#get_cell_area ~path ~col () in - let height = Gdk.Rectangle.height area in - let height = page_size * height in - height - in - let len = ref 0 in - let () = model#store#foreach (fun _ _ -> incr len; false) in - if !len > page_size then - let () = frame#set_vpolicy `ALWAYS in - data#misc#set_size_request ~height () - else - data#misc#set_size_request ~height:(-1) () + method interactive_delay = (-1) - method private refresh () = - let () = frame#set_vpolicy `NEVER in - let () = self#select_first () in - let () = obj#misc#show () in - let () = self#manage_scrollbar () in - obj#resize ~width:1 ~height:1 + method priority = 0 - method private start_callback off = - let (x, y, w, h) = self#coordinates (`OFFSET off) in - let () = obj#move ~x ~y:(y + 3 * h / 2) in - () + end in + let provider = GSourceView3.source_completion_provider provider in + object (self) - method private update_callback (off, word, props) = - if Proposals.is_empty props then self#hide () - else if Proposals.mem word props then self#hide () - else self#refresh () + inherit GSourceView3.source_completion_provider provider#as_source_completion_provider - method private end_callback () = - obj#misc#hide () + method active = !active - method private hide () = self#end_callback () + method set_active b = active := b - initializer - let move_cb _ _ ~extend = self#hide () in - let key_cb ev = - let eval cb = cb (); true in - let ev_key = GdkEvent.Key.keyval ev in - if obj#misc#visible then - if ev_key = GdkKeysyms._Up then eval self#select_previous - else if ev_key = GdkKeysyms._Down then eval self#select_next - else if ev_key = GdkKeysyms._Tab then eval self#select_enter - else if ev_key = GdkKeysyms._Return then eval self#select_enter - else if ev_key = GdkKeysyms._Escape then eval self#hide - else if ev_key = GdkKeysyms._Page_Down then eval self#select_next_page - else if ev_key = GdkKeysyms._Page_Up then eval self#select_previous_page - else if ev_key = GdkKeysyms._Home then eval self#select_first - else if ev_key = GdkKeysyms._End then eval self#select_last - else false - else false - in - (* Style handling *) - let _ = view#misc#connect#style_set ~callback:self#refresh_style in - let _ = self#refresh_style () in - let _ = data#set_resize_mode `PARENT in - let _ = frame#set_resize_mode `PARENT in - (* Callback to model *) - let _ = model#connect#start_completion ~callback:self#start_callback in - let _ = model#connect#update_completion ~callback:self#update_callback in - let _ = model#connect#end_completion ~callback:self#end_callback in - (* Popup interaction *) - let _ = view#event#connect#key_press ~callback:key_cb in - (* Hiding the popup when necessary*) - let _ = view#misc#connect#hide ~callback:obj#misc#hide in - let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in - let _ = view#connect#move_cursor ~callback:move_cb in - let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in - () + initializer + self_provider := Some (self :> GSourceView3.source_completion_provider) -end + end diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index ac9e6cd94f..020fe26cfb 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -10,27 +10,9 @@ module Proposals : sig type t end -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -class complete_model : Coq.coqtop -> GText.buffer -> +class completion_provider : Coq.coqtop -> object + inherit GSourceView3.source_completion_provider method active : bool - method connect : complete_model_signals method set_active : bool -> unit - method store : GTree.model_filter - method column : string GTree.column - method handle_proposal : Gtk.tree_path -> unit -end - -class complete_popup : complete_model -> GText.view -> -object - method coerce : GObj.widget - method proposal : string option end diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 769ce61ee1..b7a35d7e94 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -287,18 +287,17 @@ end class script_view (tv : source_view) (ct : Coq.coqtop) = let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in -let completion = new Wg_Completion.complete_model ct view#buffer in -let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in +let provider = new Wg_Completion.completion_provider ct in object (self) inherit GSourceView3.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer - method auto_complete = completion#active + method auto_complete = provider#active method set_auto_complete flag = - completion#set_active flag + provider#set_active flag method recenter_insert = self#scroll_to_mark @@ -448,7 +447,7 @@ object (self) self#buffer#delete_mark (`MARK insert_mark) - method complete_popup = popup + method proposal : string option = None (* FIXME *) method undo = undo_manager#undo method redo = undo_manager#redo @@ -527,10 +526,15 @@ object (self) stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs; stick tab_length self self#set_tab_width; stick auto_complete self self#set_auto_complete; + stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d); let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in stick text_font self cb; + let () = self#completion#set_accelerators 0 in + let () = self#completion#set_show_headers false in + let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in + () end diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 91c8e758a5..4b6591e063 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -28,7 +28,7 @@ object method uncomment : unit -> unit method apply_unicode_binding : unit -> unit method recenter_insert : unit - method complete_popup : Wg_Completion.complete_popup + method proposal : string option end val script_view : Coq.coqtop -> diff --git a/interp/impargs.ml b/interp/impargs.ml index df28b32f81..e2c732809a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -646,11 +646,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l -(* TODO: either turn these warnings on and document them, or handle these cases sensibly *) -let warn_set_maximal_deprecated = - CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated" - (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal")) +let msg_trailing_implicit id = + user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].")) type implicit_kind = Implicit | MaximallyImplicit | NotImplicit @@ -662,7 +660,7 @@ let compute_implicit_statuses autoimps l = | Name id :: autoimps, Implicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality imps' false in - if max then warn_set_maximal_deprecated i; + if max then msg_trailing_implicit id; Some (ExplByName id, Manual, (max, true)) :: imps' | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> user_err ~hdr:"set_implicits" diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 261a3510d6..cebbfe4986 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -144,11 +144,11 @@ let abstract_context hyps = in Context.Named.fold_outside fold hyps ~init:([], []) -let abstract_constant_type t (hyps, subst) = +let abstract_as_type t (hyps, subst) = let t = Vars.subst_vars subst t in List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps -let abstract_constant_body c (hyps, subst) = +let abstract_as_body c (hyps, subst) = let c = Vars.subst_vars subst c in it_mkLambda_or_LetIn c hyps @@ -192,8 +192,7 @@ let discharge_abstract_universe_context subst abs_ctx auctx = let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in subst, (AUContext.union abs_ctx auctx) -let lift_univs cb subst auctx0 = - match cb.const_universes with +let lift_univs subst auctx0 = function | Monomorphic ctx -> assert (AUContext.is_empty auctx0); subst, (Monomorphic ctx) @@ -219,7 +218,7 @@ let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) = let expmod = expmod_constr_subst cache modlist usubst in let hyps = Context.Named.map expmod abstract in let hyps = abstract_context hyps in - let c = abstract_constant_body (expmod c) hyps in + let c = abstract_as_body (expmod c) hyps in (c, priv) let cook_constr infos c = @@ -230,11 +229,11 @@ let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in - let usubst, univs = lift_univs cb usubst abs_ctx in + let usubst, univs = lift_univs usubst abs_ctx cb.const_universes in let expmod = expmod_constr_subst cache modlist usubst in let hyps0 = Context.Named.map expmod abstract in let hyps = abstract_context hyps0 in - let map c = abstract_constant_body (expmod c) hyps in + let map c = abstract_as_body (expmod c) hyps in let body = match cb.const_body with | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) @@ -243,7 +242,7 @@ let cook_constant { from = cb; info } = | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in - let typ = abstract_constant_type (expmod cb.const_type) hyps in + let typ = abstract_as_type (expmod cb.const_type) hyps in { cook_body = body; cook_type = typ; @@ -259,104 +258,160 @@ let cook_constant { from = cb; info } = (********************************) (* Discharging mutual inductive *) -(* Replace - - Var(y1)..Var(yq):C1..Cq |- Ij:Bj - Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti - - by - - |- Ij: (y1..yq:C1..Cq)Bj - I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] -*) - -let it_mkNamedProd_wo_LetIn b d = - List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d - -let abstract_inductive decls nparamdecls inds = - let open Entries in - let ntyp = List.length inds in - let ndecls = Context.Named.length decls in - let args = Context.Named.to_instance mkVar (List.rev decls) in - let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (Vars.substl subs) lc in - let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to cook_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - params +let template_level_of_var ~template_check d = + (* When [template_check], a universe from a section variable may not + be in the universes from the inductive (it must be pre-declared) + so always [None]. *) + if template_check then None + else + let c = Term.strip_prod_assum (RelDecl.get_type d) in + match kind c with + | Sort (Type u) -> Univ.Universe.level u + | _ -> None + +let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c) + +let abstract_rel_ctx (section_decls,subst) ctx = + (* Dealing with substitutions between contexts is too annoying, so + we reify [ctx] into a big [forall] term and work on that. *) + let t = it_mkProd_or_LetIn mkProp ctx in + let t = Vars.subst_vars subst t in + let t = it_mkProd_wo_LetIn t section_decls in + let ctx, t = decompose_prod_assum t in + assert (Constr.equal t mkProp); + ctx + +let abstract_lc ~ntypes expmod (newparams,subst) c = + let args = Array.rev_of_list (CList.map_filter (fun d -> + if RelDecl.is_local_def d then None + else match RelDecl.get_name d with + | Anonymous -> assert false + | Name id -> Some (mkVar id)) + newparams) in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true + let diff = List.length newparams in + let subs = List.init ntypes (fun k -> + lift diff (mkApp (mkRel (k+1), args))) + in + let c = Vars.substl subs c in + let c = Vars.subst_vars subst (expmod c) in + let c = it_mkProd_wo_LetIn c newparams in + c + +let abstract_projection ~params expmod hyps t = + let t = it_mkProd_or_LetIn t params in + let t = mkArrowR mkProp t in (* dummy type standing in for the inductive *) + let t = abstract_as_type (expmod t) hyps in + let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in + t + +let cook_one_ind ~template_check ~ntypes + (section_decls,_ as hyps) expmod mip = + let mind_arity = match mip.mind_arity with + | RegularArity {mind_user_arity=arity;mind_sort=sort} -> + let arity = abstract_as_type (expmod arity) hyps in + let sort = destSort (expmod (mkSort sort)) in + RegularArity {mind_user_arity=arity; mind_sort=sort} + | TemplateArity {template_param_levels=levels;template_level} -> + let sec_levels = CList.map_filter (fun d -> + if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d) + else None) + section_decls + in + let levels = List.rev_append sec_levels levels in + TemplateArity {template_param_levels=levels;template_level} + in + let mind_arity_ctxt = + let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in + abstract_rel_ctx hyps ctx + in + let mind_user_lc = + Array.map (abstract_lc ~ntypes expmod hyps) + mip.mind_user_lc + in + let mind_nf_lc = Array.map (fun (ctx,t) -> + let lc = it_mkProd_or_LetIn t ctx in + let lc = abstract_lc ~ntypes expmod hyps lc in + decompose_prod_assum lc) + mip.mind_nf_lc + in + { mind_typename = mip.mind_typename; + mind_arity_ctxt; + mind_arity; + mind_consnames = mip.mind_consnames; + mind_user_lc; + mind_nrealargs = mip.mind_nrealargs; + mind_nrealdecls = mip.mind_nrealdecls; + mind_kelim = mip.mind_kelim; + mind_nf_lc; + mind_consnrealargs = mip.mind_consnrealargs; + mind_consnrealdecls = mip.mind_consnrealdecls; + mind_recargs = mip.mind_recargs; (* TODO is this correct? checker should tell us. *) + mind_relevance = mip.mind_relevance; + mind_nb_constant = mip.mind_nb_constant; + mind_nb_args = mip.mind_nb_args; + mind_reloc_tbl = mip.mind_reloc_tbl; + } let cook_inductive { Opaqueproof.modlist; abstract } mib = - let open Entries in let (section_decls, subst, abs_uctx) = abstract in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx - | Polymorphic auctx -> - let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in - let subst = Univ.make_instance_subst subst in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_entry (nas, auctx) - in + let subst, mind_universes = lift_univs subst abs_uctx mib.mind_universes in let cache = RefTable.create 13 in - let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in - let inds = - Array.map_to_list - (fun mip -> - let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = discharge ty in - let lc = Array.map discharge mip.mind_user_lc in - (mip.mind_typename, - arity, template, - Array.to_list mip.mind_consnames, - Array.to_list lc)) - mib.mind_packets in - let section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | PrimRecord info -> - Some (Some (Array.map (fun (x,_,_,_) -> x) info)) - | FakeRecord -> Some None - | NotRecord -> None + let expmod = expmod_constr_subst cache modlist subst in + let section_decls = Context.Named.map expmod section_decls in + let removed_vars = Context.Named.to_vars section_decls in + let section_decls, _ as hyps = abstract_context section_decls in + let nnewparams = Context.Rel.nhyps section_decls in + let template_check = mib.mind_typing_flags.check_template in + let mind_params_ctxt = + let ctx = Context.Rel.map expmod mib.mind_params_ctxt in + abstract_rel_ctx hyps ctx + in + let ntypes = mib.mind_ntypes in + let mind_packets = + Array.map (cook_one_ind ~template_check ~ntypes hyps expmod) + mib.mind_packets in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_cumulative = Option.has_some mib.mind_variance; - mind_entry_universes = ind_univs + let mind_record = match mib.mind_record with + | NotRecord -> NotRecord + | FakeRecord -> FakeRecord + | PrimRecord data -> + let data = Array.map (fun (id,projs,relevances,tys) -> + let tys = Array.map (abstract_projection ~params:mib.mind_params_ctxt expmod hyps) tys in + (id,projs,relevances,tys)) + data + in + PrimRecord data + in + let mind_hyps = + List.filter (fun d -> not (Id.Set.mem (NamedDecl.get_id d) removed_vars)) + mib.mind_hyps + in + let mind_variance, mind_sec_variance = + match mib.mind_variance, mib.mind_sec_variance with + | None, None -> None, None + | None, Some _ | Some _, None -> assert false + | Some variance, Some sec_variance -> + let sec_variance, newvariance = + Array.chop (Array.length sec_variance - AUContext.size abs_uctx) + sec_variance + in + Some (Array.append newvariance variance), Some sec_variance + in + { + mind_packets; + mind_record; + mind_finite = mib.mind_finite; + mind_ntypes = mib.mind_ntypes; + mind_hyps; + mind_nparams = mib.mind_nparams + nnewparams; + mind_nparams_rec = mib.mind_nparams_rec + nnewparams; + mind_params_ctxt; + mind_universes; + mind_variance; + mind_sec_variance; + mind_private = mib.mind_private; + mind_typing_flags = mib.mind_typing_flags; } let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 83a8b9edfc..c2d47735ec 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -31,7 +31,7 @@ val cook_constr : Opaqueproof.cooking_info list -> (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) val cook_inductive : - Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry + Opaqueproof.cooking_info -> mutual_inductive_body -> mutual_inductive_body (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9fd10b32e6..0b6e59bd5e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -223,6 +223,11 @@ type mutual_inductive_body = { mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) + mind_sec_variance : Univ.Variance.t array option; + (** Variance info for section polymorphic universes. [None] + outside sections. The final variance once all sections are + discharged is [mind_sec_variance ++ mind_variance]. *) + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 35185b6a5e..27e3f84464 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -248,6 +248,7 @@ let subst_mind_body sub mib = mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; mind_variance = mib.mind_variance; + mind_sec_variance = mib.mind_sec_variance; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d9ccf81619..591cd050a5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -197,16 +197,14 @@ let unbounded_from_below u cstrs = is u_k and is contributing. *) let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = let check_level l = - if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && - unbounded_from_below l (Univ.ContextSet.constraints uctx) && - not (Univ.LSet.mem l ctor_levels) then - Some l - else None + Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + unbounded_from_below l (Univ.ContextSet.constraints uctx) && + not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in let univs = if template_check then - Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs else univs (* Doesn't check the universes can be generalized *) in let fold acc = function @@ -278,7 +276,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let typecheck_inductive env (mie:mutual_inductive_entry) = +let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") | _ -> () @@ -337,8 +335,19 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = data, Some None in - (* TODO pass only the needed bits *) - let variance = InferCumulativity.infer_inductive env mie in + let variance = if not mie.mind_entry_cumulative then None + else match mie.mind_entry_universes with + | Monomorphic_entry _ -> + CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.") + | Polymorphic_entry (_,uctx) -> + let univs = Instance.to_array @@ UContext.instance uctx in + let univs = match sec_univs with + | None -> univs + | Some sec_univs -> Array.append sec_univs univs + in + let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in + Some variances + in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 5c04e860a2..8dea8f046d 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -17,6 +17,7 @@ open Declarations - environment with inductives + parameters in rel context - abstracted universes - checked variance info + (variance for section universes is at the beginning of the array) - record entry (checked to be OK) - parameters - for each inductive, @@ -24,9 +25,11 @@ open Declarations * (indices * splayed constructor types) (both without params) * top allowed elimination *) -val typecheck_inductive : env -> mutual_inductive_entry -> - env - * universes * Univ.Variance.t array option +val typecheck_inductive : env -> sec_univs:Univ.Level.t array option + -> mutual_inductive_entry + -> env + * universes + * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context * ((inductive_arity * Constr.types array) * diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ab915e2b8d..3771454db5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -466,7 +466,8 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env ~sec_univs names prv univs variance + paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env paramsctxt inds in @@ -487,18 +488,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in - let transf num = - let arity = List.length (dest_subterms recarg).(num) in - if Int.equal arity 0 then - let p = (!nconst, 0) in - incr nconst; p - else - let p = (!nblock + 1, arity) in - incr nblock; p - (* les tag des constructeur constant commence a 0, - les tag des constructeur non constant a 1 (0 => accumulator) *) + let transf arity = + if Int.equal arity 0 then + let p = (!nconst, 0) in + incr nconst; p + else + let p = (!nblock + 1, arity) in + incr nblock; p + (* les tag des constructeur constant commence a 0, + les tag des constructeur non constant a 1 (0 => accumulator) *) in - let rtbl = Array.init (List.length cnames) transf in + let rtbl = Array.map transf consnrealargs in (* Build the inductive packet *) { mind_typename = id; mind_arity = arity; @@ -518,6 +518,15 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_reloc_tbl = rtbl; } in let packets = Array.map3 build_one_packet names inds recargs in + let variance, sec_variance = match variance with + | None -> None, None + | Some variance -> match sec_univs with + | None -> Some variance, None + | Some sec_univs -> + let nsec = Array.length sec_univs in + Some (Array.sub variance nsec (Array.length variance - nsec)), + Some (Array.sub variance 0 nsec) + in let mib = (* Build the mutual inductive *) { mind_record = NotRecord; @@ -530,6 +539,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_packets = packets; mind_universes = univs; mind_variance = variance; + mind_sec_variance = sec_variance; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -550,9 +560,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (************************************************************************) (************************************************************************) -let check_inductive env kn mie = +let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in + let (env_ar_par, univs, variance, record, paramsctxt, inds) = + IndTyping.typecheck_inductive env ~sec_univs mie + in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_positive in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) @@ -563,6 +575,6 @@ let check_inductive env kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 240ba4e2bb..9b54e8b878 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,4 +14,5 @@ open Environ open Entries (** Check an inductive. *) -val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body +val check_inductive : env -> sec_univs:Univ.Level.t array option + -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 77abe6b410..211c909241 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -188,15 +188,12 @@ let infer_arity_constructor is_arity env variances arcn = open Entries -let infer_inductive_core env params entries uctx = - let uarray = Instance.to_array @@ UContext.instance uctx in - if Array.is_empty uarray then raise TrivialVariance; - let env = Environ.push_context uctx env in +let infer_inductive_core env univs entries = + if Array.is_empty univs then raise TrivialVariance; let variances = Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) - LMap.empty uarray + LMap.empty univs in - let env, _ = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity @@ -210,17 +207,8 @@ let infer_inductive_core env params entries uctx = | exception Not_found -> Invariant | IrrelevantI -> Irrelevant | CovariantI -> Covariant) - uarray - -let infer_inductive env mie = - let open Entries in - let params = mie.mind_entry_params in - let entries = mie.mind_entry_inds in - if not mie.mind_entry_cumulative then None - else - let uctx = match mie.mind_entry_universes with - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> uctx - in - try Some (infer_inductive_core env params entries uctx) - with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) + univs + +let infer_inductive ~env_params univs entries = + try infer_inductive_core env_params univs entries + with TrivialVariance -> Array.make (Array.length univs) Invariant diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index 2bddfe21e2..a8f593c7f9 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -8,5 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> - Univ.Variance.t array option +val infer_inductive + : env_params:Environ.env + (** Environment containing the polymorphic universes and the + parameters. *) + -> Univ.Level.t array + (** Universes whose cumulativity we want to infer. *) + -> Entries.one_inductive_entry list + (** The inductive block data we want to infer cumulativity for. + NB: we ignore the template bool and the names, only the terms + are used. *) + -> Univ.Variance.t array diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1cef729916..a62b51e8aa 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -27,15 +27,35 @@ let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) let output_dir = ".coq-native" -(* Extension of genereted ml files, stored for debugging purposes *) +(* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" let ( / ) = Filename.concat -(* We have to delay evaluation of include_dirs because coqlib cannot be guessed -until flags have been properly initialized *) +(* Directory for temporary files for the conversion and normalisation + (as opposed to compiling the library itself, which uses [output_dir]). *) +let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") + +let () = at_exit (fun () -> + if Lazy.is_val my_temp_dir then + try + let d = Lazy.force my_temp_dir in + Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); + Unix.rmdir d + with e -> + Feedback.msg_warning + Pp.(str "Native compile: failed to cleanup: " ++ + str(Printexc.to_string e) ++ fnl())) + +(* We have to delay evaluation of include_dirs because coqlib cannot + be guessed until flags have been properly initialized. It also lets + us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file + without native compute or native conv uses). *) let include_dirs () = - [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] + let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in + if Lazy.is_val my_temp_dir + then (Lazy.force my_temp_dir) :: base + else base (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun _x -> () : string -> unit) @@ -44,7 +64,8 @@ let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) let get_ml_filename () = - let filename = Filename.temp_file "Coq_native" source_ext in + let temp_dir = Lazy.force my_temp_dir in + let filename = Filename.temp_file ~temp_dir "Coq_native" source_ext in let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in filename, prefix diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ee101400d6..f6f2058c13 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -908,14 +908,19 @@ let check_mind mie lab = (* The label and the first inductive type name should match *) assert (Id.equal (Label.to_id lab) oie.mind_entry_typename) +let add_checked_mind kn mib senv = + let mib = + match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + in + add_field (MutInd.label kn,SFBmind mib) (I kn) senv + let add_mind l mie senv = let () = check_mind mie l in let kn = MutInd.make2 senv.modpath l in - let mib = Indtypes.check_inductive senv.env kn mie in - let mib = - match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + let sec_univs = Option.map Section.all_poly_univs senv.sections in - kn, add_field (l,SFBmind mib) (I kn) senv + let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in + kn, add_checked_mind kn mib senv (** Insertion of module types *) @@ -1014,9 +1019,8 @@ let close_section senv = add_constant_aux senv (kn, cb) | `Inductive (ind, mib) -> let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in - let mie = Cooking.cook_inductive info mib in - let _, senv = add_mind (MutInd.label ind) mie senv in - senv + let mib = Cooking.cook_inductive info mib in + add_checked_mind ind mib senv in List.fold_left fold senv redo diff --git a/kernel/section.ml b/kernel/section.ml index 603ef5d006..6fa0543b23 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -28,6 +28,8 @@ type 'a t = { sec_mono_universes : ContextSet.t; sec_poly_universes : Name.t array * UContext.t; (** Universes local to the section *) + all_poly_univs : Univ.Level.t array; + (** All polymorphic universes, including from previous sections. *) has_poly_univs : bool; (** Are there polymorphic universes or constraints, including in previous sections. *) sec_entries : section_entry list; @@ -41,6 +43,8 @@ let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth p let has_poly_univs sec = sec.has_poly_univs +let all_poly_univs sec = sec.all_poly_univs + let find_emap e (cmap, imap) = match e with | SecDefinition con -> Cmap.find con cmap | SecInductive ind -> Mindmap.find ind imap @@ -57,7 +61,10 @@ let push_context (nas, ctx) sec = else let (snas, sctx) = sec.sec_poly_universes in let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in - { sec with sec_poly_universes; has_poly_univs = true } + let all_poly_univs = + Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx) + in + { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true } let rec is_polymorphic_univ u sec = let (_, uctx) = sec.sec_poly_universes in @@ -81,6 +88,7 @@ let open_section ~custom sec_prev = sec_context = 0; sec_mono_universes = ContextSet.empty; sec_poly_universes = ([||], UContext.empty); + all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev; has_poly_univs = Option.cata has_poly_univs false sec_prev; sec_entries = []; sec_data = (Cmap.empty, Mindmap.empty); diff --git a/kernel/section.mli b/kernel/section.mli index fbd3d8254e..37d0dab317 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -57,6 +57,14 @@ val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t (** {6 Retrieving section data} *) +val all_poly_univs : 'a t -> Univ.Level.t array +(** Returns all polymorphic universes, including those from previous + sections. Earlier sections are earlier in the array. + + NB: even if the array is empty there may be polymorphic + constraints about monomorphic universes, which prevent declaring + monomorphic globals. *) + type abstr_info = private { abstr_ctx : Constr.named_context; (** Section variables of this prefix *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 0029ff96d5..0712774576 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -345,8 +345,8 @@ struct (Level.is_prop u && not (Level.is_sprop v)) else false - let successor (u,n) = - if Level.is_small u then type1 + let successor (u,n as e) = + if is_small e then type1 else (u, n + 1) let addn k (u,n as x) = @@ -755,6 +755,10 @@ struct | Invariant, _ | _, Invariant -> Invariant | Covariant, Covariant -> Covariant + let equal a b = match a,b with + | Irrelevant, Irrelevant | Covariant, Covariant | Invariant, Invariant -> true + | (Irrelevant | Covariant | Invariant), _ -> false + let check_subtype x y = match x, y with | (Irrelevant | Covariant | Invariant), Irrelevant -> true | Irrelevant, Covariant -> false diff --git a/kernel/univ.mli b/kernel/univ.mli index ccb5c80cbf..f7c984870f 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -263,6 +263,8 @@ sig val pr : t -> Pp.t + val equal : t -> t -> bool + end (** {6 Universe instances} *) @@ -320,7 +322,7 @@ val in_punivs : 'a -> 'a puniverses val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool (** A vector of universe levels with universe Constraint.t, - representiong local universe variables and associated Constraint.t *) + representing local universe variables and associated Constraint.t *) module UContext : sig diff --git a/lib/future.ml b/lib/future.ml index d3ea538549..5cccd2038d 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -12,13 +12,13 @@ let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing and don't pass \"-quick\" to "^ + "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) let not_here_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ - "asynchronous script processing and don't pass \"-quick\" to "^ + "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) let customize_not_ready_msg f = not_ready_msg := f diff --git a/plugins/extraction/ExtrOcamlChar.v b/plugins/extraction/ExtrOcamlChar.v new file mode 100644 index 0000000000..1e68365dd3 --- /dev/null +++ b/plugins/extraction/ExtrOcamlChar.v @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Extraction to Ocaml : extract ascii to OCaml's char type *) + +Require Coq.extraction.Extraction. + +Require Import Ascii String Coq.Strings.Byte. + +Extract Inductive ascii => char +[ +"(* If this appears, you're using Ascii internals. Please don't *) + (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> + let f b i = if b then 1 lsl i else 0 in + Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" +] +"(* If this appears, you're using Ascii internals. Please don't *) + (fun f c -> + let n = Char.code c in + let h i = (n land (1 lsl i)) <> 0 in + f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". + +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => + "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". + +Extract Inlined Constant ascii_dec => "(=)". +Extract Inlined Constant Ascii.eqb => "(=)". + +(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) +Extract Inductive byte => char +["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. + +Extract Inlined Constant Byte.eqb => "(=)". +Extract Inlined Constant Byte.byte_eq_dec => "(=)". +Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v new file mode 100644 index 0000000000..ec3da1e444 --- /dev/null +++ b/plugins/extraction/ExtrOcamlNativeString.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Extraction to Ocaml : extract ascii to OCaml's char type + and string to OCaml's string type. *) + +Require Coq.extraction.Extraction. + +Require Import Ascii String Coq.Strings.Byte. +Require Export ExtrOcamlChar. + +(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) +Extract Inductive byte => char +["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. + +Extract Inlined Constant Byte.eqb => "(=)". +Extract Inlined Constant Byte.byte_eq_dec => "(=)". +Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". + +(* This differs from ExtrOcamlString.v: the latter extracts "string" + to "char list", and we extract "string" to "string" *) + +Extract Inductive string => "string" +[ +(* EmptyString *) +"(* If this appears, you're using String internals. Please don't *) + """" +" +(* String *) +"(* If this appears, you're using String internals. Please don't *) + (fun (c, s) -> String.make 1 c ^ s) +" +] +"(* If this appears, you're using String internals. Please don't *) + (fun f0 f1 s -> + let l = String.length s in + if l = 0 then f0 else f1 (String.get s 0) (String.sub s 1 (l-1))) +". + +Extract Inlined Constant String.string_dec => "(=)". +Extract Inlined Constant String.eqb => "(=)". +Extract Inlined Constant String.append => "(^)". +Extract Inlined Constant String.concat => "String.concat". +Extract Inlined Constant String.prefix => + "(fun s1 s2 -> + let l1 = String.length s1 and l2 = String.length s2 in + l1 <= l2 && String.sub s2 0 l1 = s1)". +Extract Inlined Constant String.string_of_list_ascii => + "(fun l -> + let a = Array.of_list l in + String.init (Array.length a) (fun i -> a.(i)))". +Extract Inlined Constant String.list_ascii_of_string => + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". +Extract Inlined Constant String.string_of_list_byte => + "(fun l -> + let a = Array.of_list l in + String.init (Array.length a) (fun i -> a.(i)))". +Extract Inlined Constant String.list_byte_of_string => + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". + +(* Other operations in module String (at the time of this writing): + String.length + String.get + String.substring + String.index + String.findex + They all use type "nat". If we know that "nat" extracts + to O | S of nat, we can provide OCaml implementations + for these functions that work directly on OCaml's strings. + However "nat" could be extracted to other OCaml types... +*) + +(* +Definition test := "ceci est un test"%string. + +Recursive Extraction test Ascii.zero Ascii.one. +*) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 6265a67577..18c5ed3fe4 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -13,43 +13,6 @@ Require Coq.extraction.Extraction. Require Import Ascii String Coq.Strings.Byte. - -Extract Inductive ascii => char -[ -"(* If this appears, you're using Ascii internals. Please don't *) - (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> - let f b i = if b then 1 lsl i else 0 in - Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" -] -"(* If this appears, you're using Ascii internals. Please don't *) - (fun f c -> - let n = Char.code c in - let h i = (n land (1 lsl i)) <> 0 in - f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". - -Extract Constant zero => "'\000'". -Extract Constant one => "'\001'". -Extract Constant shift => - "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". - -Extract Inlined Constant ascii_dec => "(=)". -Extract Inlined Constant Ascii.eqb => "(=)". +Require Export ExtrOcamlChar. Extract Inductive string => "char list" [ "[]" "(::)" ]. - -(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) -Extract Inductive byte => char -["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. - -Extract Inlined Constant Byte.eqb => "(=)". -Extract Inlined Constant Byte.byte_eq_dec => "(=)". -Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". -Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". - -(* -Definition test := "ceci est un test"%string. -Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)). -Definition test3 := List.map ascii_of_nat (List.seq 0 256). - -Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect. -*) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 2f3f42c5f6..29da12de40 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -14,7 +14,6 @@ open Names open ModPath open Namegen open Nameops -open Libnames open Table open Miniml open Mlutil @@ -616,10 +615,15 @@ let pp_module mp = [Extract Inductive ascii => char] has been declared, then the constants are directly turned into chars *) -let mk_ind path s = - MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s) +let ascii_type_name = "core.ascii.type" +let ascii_constructor_name = "core.ascii.ascii" -let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" +let is_ascii_registered () = + Coqlib.has_ref ascii_type_name + && Coqlib.has_ref ascii_constructor_name + +let ascii_type_ref () = Coqlib.lib_ref ascii_type_name +let ascii_constructor_ref () = Coqlib.lib_ref ascii_constructor_name let check_extract_ascii () = try @@ -628,15 +632,18 @@ let check_extract_ascii () = | Haskell -> "Prelude.Char" | _ -> raise Not_found in - String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type) + String.equal (find_custom @@ ascii_type_ref ()) (char_type) with Not_found -> false let is_list_cons l = List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l let is_native_char = function - | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) -> - MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l + | MLcons(_,gr,l) -> + is_ascii_registered () + && GlobRef.equal gr (ascii_constructor_ref ()) + && check_extract_ascii () + && is_list_cons l | _ -> false let get_native_char c = @@ -649,3 +656,84 @@ let get_native_char c = Char.chr (cumul l) let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'") + +(** Special hack for constants of type String.string : if an + [Extract Inductive string => string] has been declared, then + the constants are directly turned into string literals *) + +let string_type_name = "core.string.type" +let empty_string_name = "core.string.empty" +let string_constructor_name = "core.string.string" + +let is_string_registered () = + Coqlib.has_ref string_type_name + && Coqlib.has_ref empty_string_name + && Coqlib.has_ref string_constructor_name + +let string_type_ref () = Coqlib.lib_ref string_type_name +let empty_string_ref () = Coqlib.lib_ref empty_string_name +let string_constructor_ref () = Coqlib.lib_ref string_constructor_name + +let check_extract_string () = + try + let string_type = match lang () with + | Ocaml -> "string" + | Haskell -> "Prelude.String" + | _ -> raise Not_found + in + String.equal (find_custom @@ string_type_ref ()) string_type + with Not_found -> false + +(* The argument is known to be of type Coq.Strings.String.string. + Check that it is built from constructors EmptyString and String + with constant ascii arguments. *) + +let rec is_native_string_rec empty_string_ref string_constructor_ref = function + (* "EmptyString" constructor *) + | MLcons(_, gr, []) -> GlobRef.equal gr empty_string_ref + (* "String" constructor *) + | MLcons(_, gr, [hd; tl]) -> + GlobRef.equal gr string_constructor_ref + && is_native_char hd + && is_native_string_rec empty_string_ref string_constructor_ref tl + (* others *) + | _ -> false + +(* Here we first check that the argument is the type registered as + core.string.type and that extraction to native strings was + requested. Then we check every character via + [is_native_string_rec]. *) + +let is_native_string c = + match c with + | MLcons(_, GlobRef.ConstructRef(ind, j), l) -> + is_string_registered () + && GlobRef.equal (GlobRef.IndRef ind) (string_type_ref ()) + && check_extract_string () + && is_native_string_rec (empty_string_ref ()) (string_constructor_ref ()) c + | _ -> false + +(* Extract the underlying string. *) + +let get_native_string c = + let buf = Buffer.create 64 in + let rec get = function + (* "EmptyString" constructor *) + | MLcons(_, gr, []) when GlobRef.equal gr (empty_string_ref ()) -> + Buffer.contents buf + (* "String" constructor *) + | MLcons(_, gr, [hd; tl]) when GlobRef.equal gr (string_constructor_ref ()) -> + Buffer.add_char buf (get_native_char hd); + get tl + (* others *) + | _ -> assert false + in get c + +(* Printing the underlying string. *) + +let pp_native_string c = + str ("\"" ^ String.escaped (get_native_string c) ^ "\"") + +(* Registered sig type *) + +let sig_type_ref () = Coqlib.lib_ref "core.sig.type" diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index e4e9c4c527..9dbc09dd06 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -70,10 +70,6 @@ val reset_renaming_tables : reset_kind -> unit val set_keywords : Id.Set.t -> unit -(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) - -val mk_ind : string -> string -> MutInd.t - (** Special hack for constants of type Ascii.ascii : if an [Extract Inductive ascii => char] has been declared, then the constants are directly turned into chars *) @@ -81,3 +77,14 @@ val mk_ind : string -> string -> MutInd.t val is_native_char : ml_ast -> bool val get_native_char : ml_ast -> char val pp_native_char : ml_ast -> Pp.t + +(** Special hack for constants of type String.string : if an + [Extract Inductive string => string] has been declared, then + the constants are directly turned into string literals *) + +val is_native_string : ml_ast -> bool +val get_native_string : ml_ast -> string +val pp_native_string : ml_ast -> Pp.t + +(* Registered sig type *) +val sig_type_ref : unit -> GlobRef.t diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f0053ba6b5..eef050efbd 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -109,8 +109,8 @@ let rec pp_type par vl t = (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + | Tglob (gr,l) + when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) -> pp_type true vl (List.hd l) | Tglob (r,l) -> pp_par par @@ -171,6 +171,7 @@ let rec pp_expr par env args = assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c + | _ when is_native_string c -> pp_native_string c | [] -> pp_global Cons r | [a] -> pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 66429833b9..97cad87825 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -165,8 +165,8 @@ let pp_type par vl t = | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r - | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + | Tglob (gr,l) + when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) -> pp_tuple_light pp_rec l | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r @@ -249,6 +249,7 @@ let rec pp_expr par env args = assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c + | _ when is_native_string c -> pp_native_string c | [a1;a2] when is_infix r -> let pp = pp_expr true env [] in pp_par par (pp a1 ++ str (get_infix r) ++ pp a2) diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v index 785a53fafa..18cd196148 100644 --- a/plugins/micromega/Zify.v +++ b/plugins/micromega/Zify.v @@ -87,4 +87,4 @@ Ltac applySpec S := (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook. +Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook. diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index 97f6fe0613..edfb5a2a94 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -523,3 +523,22 @@ Instance SatProdPos : Saturate Z.mul := SatOk := Z.mul_pos_pos |}. Add Saturate SatProdPos. + +Lemma pow_pos_strict : + forall a b, + 0 < a -> 0 < b -> 0 < a ^ b. +Proof. + intros. + apply Z.pow_pos_nonneg; auto. + apply Z.lt_le_incl;auto. +Qed. + + +Instance SatPowPos : Saturate Z.pow := + {| + PArg1 := fun x => 0 < x; + PArg2 := fun y => 0 < y; + PRes := fun r => 0 < r; + SatOk := pow_pos_strict + |}. +Add Saturate SatPowPos. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index cb15274736..61234145e1 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -395,50 +395,40 @@ let saturate_by_linear_equalities sys = output_sys sys output_sys sys'; sys' -(* let saturate_linear_equality_non_linear sys0 = - let (l,_) = extract_all (is_substitution false) sys0 in - let rec elim l acc = - match l with - | [] -> acc - | (v,pc)::l' -> - let nc = saturate (non_linear_pivot sys0 pc v) (sys0@acc) in - elim l' (nc@acc) in - elim l [] - *) - -let bounded_vars (sys : WithProof.t list) = - let l = fst (extract_all (fun ((p, o), prf) -> LinPoly.is_variable p) sys) in - List.fold_left (fun acc (i, wp) -> IMap.add i wp acc) IMap.empty l - -let rec power n p = if n = 1 then p else WithProof.product p (power (n - 1) p) - -let bound_monomial mp m = - if Monomial.is_var m || Monomial.is_const m then None - else - try - Some - (Monomial.fold - (fun v i acc -> - let wp = IMap.find v mp in - WithProof.product (power i wp) acc) - m (WithProof.const (Int 1))) - with Not_found -> None - let bound_monomials (sys : WithProof.t list) = - let mp = bounded_vars sys in - let m = + let l = + extract_all + (fun ((p, o), _) -> + match LinPoly.get_bound p with + | None -> None + | Some Vect.Bound.{cst; var; coeff} -> + Some (Monomial.degree (LinPoly.MonT.retrieve var))) + sys + in + let deg = + List.fold_left (fun acc ((p, o), _) -> max acc (LinPoly.degree p)) 0 sys + in + let vars = List.fold_left - (fun acc ((p, _), _) -> - Vect.fold - (fun acc v _ -> - let m = LinPoly.MonT.retrieve v in - match bound_monomial mp m with - | None -> acc - | Some r -> IMap.add v r acc) - acc p) - IMap.empty sys + (fun acc ((p, o), _) -> ISet.union (LinPoly.monomials p) acc) + ISet.empty sys + in + let bounds = + saturate_bin + (fun (i1, w1) (i2, w2) -> + if i1 + i2 > deg then None + else + match WithProof.mul_bound w1 w2 with + | None -> None + | Some b -> Some (i1 + i2, b)) + (fst l) + in + let has_mon (_, ((p, o), _)) = + match LinPoly.get_bound p with + | None -> false + | Some Vect.Bound.{cst; var; coeff} -> ISet.mem var vars in - IMap.fold (fun _ e acc -> e :: acc) m [] + List.map snd (List.filter has_mon bounds) @ snd l let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 66f263c0b1..2b5fac32a2 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -34,12 +34,13 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF END TACTIC EXTEND ITER -| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t } +| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t } END TACTIC EXTEND TRANS | [ "zify_op" ] -> { Zify.zify_tac } -| [ "saturate" ] -> { Zify.saturate } +| [ "zify_saturate" ] -> { Zify.saturate } +| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t } END VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 03f042647c..160b492d3d 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -140,6 +140,25 @@ let saturate p f sys = Printexc.print_backtrace stdout; raise x +let saturate_bin (f : 'a -> 'a -> 'a option) (l : 'a list) = + let rec map_with acc e l = + match l with + | [] -> acc + | e' :: l' -> ( + match f e e' with + | None -> map_with acc e l' + | Some r -> map_with (r :: acc) e l' ) + in + let rec map2_with acc l' = + match l' with [] -> acc | e' :: l' -> map2_with (map_with acc e' l) l' + in + let rec iterate acc l' = + match map2_with [] l' with + | [] -> List.rev_append l' acc + | res -> iterate (List.rev_append l' acc) res + in + iterate [] l + open Num open Big_int diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index ef8d154b13..5dcaf3be44 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -116,6 +116,7 @@ val simplify : ('a -> 'a option) -> 'a list -> 'a list option val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list +val saturate_bin : ('a -> 'a -> 'a option) -> 'a list -> 'a list val generate : ('a -> 'b option) -> 'a list -> 'b list val app_funs : ('a -> 'b option) list -> 'a -> 'b option val command : string -> string array -> 'a -> 'b diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index a4f9b60b14..b20213979b 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -379,6 +379,8 @@ module LinPoly = struct else acc) [] l + let get_bound p = Vect.Bound.of_vect p + let min_list (l : int list) = match l with [] -> None | e :: l -> Some (List.fold_left min e l) @@ -892,8 +894,9 @@ module WithProof = struct if Vect.is_null r && n >/ Int 0 then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) else ( - Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output - ((p1, o1), prf1); + if debug then + Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output + ((p1, o1), prf1); raise InvalidProof ) let cutting_plane ((p, o), prf) = @@ -1027,6 +1030,31 @@ module WithProof = struct else None in saturate select gen sys0 + + open Vect.Bound + + let mul_bound w1 w2 = + let (p1, o1), prf1 = w1 in + let (p2, o2), prf2 = w2 in + match (LinPoly.get_bound p1, LinPoly.get_bound p2) with + | None, _ | _, None -> None + | ( Some {cst = c1; var = v1; coeff = c1'} + , Some {cst = c2; var = v2; coeff = c2'} ) -> ( + let good_coeff b o = + match o with + | Eq -> Some (minus_num b) + | _ -> if b <=/ Int 0 then Some (minus_num b) else None + in + match (good_coeff c1 o2, good_coeff c2 o1) with + | None, _ | _, None -> None + | Some c1, Some c2 -> + let ext_mult c w = + if c =/ Int 0 then zero else mult (LinPoly.constant c) w + in + Some + (addition + (addition (product w1 w2) (ext_mult c1 w2)) + (ext_mult c2 w1)) ) end (* Local Variables: *) diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 7e905ac69b..4b56b037e0 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -224,6 +224,8 @@ module LinPoly : sig p is linear in x i.e x does not occur in b and a is a constant such that [pred a] *) + val get_bound : t -> Vect.Bound.t option + val product : t -> t -> t (** [product p q] @return the product of the polynomial [p*q] *) @@ -372,4 +374,5 @@ module WithProof : sig val saturate_subst : bool -> t list -> t list val is_substitution : bool -> t -> var option + val mul_bound : t -> t -> t option end diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 5d8ae83853..e71c89b4db 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -965,6 +965,43 @@ let trans_concl t = let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' +let assert_inj t = + init_cache (); + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd t); + Tacticals.New.tclIDTAC + with Not_found -> + Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist")) + +let do_let tac (h : Constr.named_declaration) = + match h with + | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC + | Context.Named.Declaration.LocalDef (id, t, ty) -> + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd (EConstr.of_constr ty)); + tac id.Context.binder_name t ty + with Not_found -> Tacticals.New.tclIDTAC) + +let iter_let tac = + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let sign = Environ.named_context env in + Tacticals.New.tclMAP (do_let tac) sign) + +let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) = + init_cache (); + iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) -> + Ltac_plugin.Tacinterp.Value.apply tac + [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ]) + let zify_tac = Proofview.Goal.enter (fun gl -> Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"]; diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 9e3cf5d24c..4930a845c9 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -27,3 +27,5 @@ module Saturate : S val zify_tac : unit Proofview.tactic val saturate : unit Proofview.tactic val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val assert_inj : EConstr.constr -> unit Proofview.tactic +val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index f5d53cbbf3..34533670f8 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -573,27 +573,16 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. - -(** [is_inj T] returns true iff the type T has an injection *) -Ltac is_inj T := - match T with - | _ => let x := constr:(_ : InjTyp T _ ) in true - | _ => false - end. - (* [elim_let] replaces a let binding (x := e : t) by an equation (x = e) if t is an injected type *) -Ltac elim_let := - repeat - match goal with - | x := ?t : ?ty |- _ => - let b := is_inj ty in - match b with - | true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - end - end. +Ltac elim_binding x t ty := + let h := fresh "heq_" x in + pose proof (@eq_refl ty x : @eq ty x t) as h; + try clearbody x. + +Ltac elim_let := zify_iter_let elim_binding. Ltac zify := intros ; elim_let ; - Zify.zify ; ZifyInst.saturate. + Zify.zify ; ZifyInst.zify_saturate. diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 35e182840b..3b918b5396 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,6 @@ open CErrors open Util open Pp open Names -open Globnames open Constr open Mod_subst open Reductionops @@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) = (Option.Smart.map (subst_constant subst)) projs in - let id' = subst_constructor subst id in + let id' = Globnames.subst_constructor subst id in if projs' == projs && id' == id then obj else (id',kl,projs') @@ -139,7 +138,7 @@ let find_primitive_projection c = *) type obj_typ = { - o_ORIGIN : Constant.t; + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -190,13 +189,13 @@ let rec cs_pattern_of_constr env t = let _, params = Inductive.find_rectype env ty in Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> Const_cs (global_of_constr t) , None, [] + | _ -> Const_cs (Globnames.global_of_constr t) , None, [] let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (sign,env,t,con,proji_sp) -> + (fun (sign,env,t,ref,proji_sp) -> let env = Termops.push_rels_assum sign env in - let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in + let con_pp = Nametab.pr_global_env Id.Set.empty ref in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " @@ -204,11 +203,17 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections env ~warn (con,ind) = - let o_CTX = Environ.constant_context env con in - let u = Univ.make_abstract_instance o_CTX in - let o_DEF = mkConstU (con, u) in - let c = Environ.constant_value_in env (con,u) in +let compute_canonical_projections env ~warn (gref,ind) = + let o_CTX = Environ.universes_of_global env gref in + let o_DEF, c = + match gref with + | GlobRef.ConstRef con -> + let u = Univ.make_abstract_instance o_CTX in + mkConstU (con, u), Environ.constant_value_in env (con,u) + | GlobRef.VarRef id -> + mkVar id, Option.get (Environ.named_body id env) + | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false + in let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in @@ -227,10 +232,10 @@ let compute_canonical_projections env ~warn (con,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> - if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); + if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); acc ) acc spopt else acc @@ -266,12 +271,17 @@ let register_canonical_structure ~warn env sigma o = warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) ) -let subst_canonical_structure subst (cst,ind as obj) = +type cs = GlobRef.t * inductive + +let subst_canonical_structure subst (gref,ind as obj) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - let cst' = subst_constant subst cst in - let ind' = subst_ind subst ind in - if cst' == cst && ind' == ind then obj else (cst',ind') + match gref with + | GlobRef.ConstRef cst -> + let cst' = subst_constant subst cst in + let ind' = subst_ind subst ind in + if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind') + | _ -> assert false (*s High-level declaration of a canonical structure *) @@ -282,15 +292,20 @@ let error_not_structure ref description = description)) let check_and_decompose_canonical_structure env sigma ref = - let sp = + let vc = match ref with - GlobRef.ConstRef sp -> sp - | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") + | GlobRef.ConstRef sp -> + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in + begin match Environ.constant_opt_value_in env (sp, u) with + | Some vc -> vc + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.VarRef id -> + begin match Environ.named_body id env with + | Some b -> b + | None -> error_not_structure ref (str "Could not find its value in the global environment.") end + | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> + error_not_structure ref (str "Expected an instance of a record or structure.") in - let u = Univ.make_abstract_instance (Environ.constant_context env sp) in - let vc = match Environ.constant_opt_value_in env (sp, u) with - | Some vc -> vc - | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with @@ -308,7 +323,7 @@ let check_and_decompose_canonical_structure env sigma ref = let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); - (sp,indsp) + (ref,indsp) let lookup_canonical_conversion (proj,pat) = assoc_pat pat (GlobRef.Map.find proj !object_table) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index aaba7cc3e5..fd156adc2c 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -73,7 +73,7 @@ type cs_pattern = | Default_cs type obj_typ = { - o_ORIGIN : Constant.t; + o_ORIGIN : GlobRef.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) @@ -87,13 +87,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t +type cs = GlobRef.t * inductive + val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> - Constant.t * inductive -> unit -val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive + cs -> unit +val subst_canonical_structure : Mod_subst.substitution -> cs -> cs val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list -val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive +val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs diff --git a/tactics/declare.ml b/tactics/declare.ml index da4de3df77..9a14f4d40f 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -362,7 +362,7 @@ let inVariable : unit -> obj = classify_function = (fun () -> Dispose)} let declare_variable ~name ~kind d = - (* Constr raisonne sur les noms courts *) + (* Variables are distinguished by only short names *) if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9258a75461..f6f7c71dfd 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2977,6 +2977,13 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) +(* This applies (f i) to all elements of ctxt where the debrujn i is + free (so it is lifted at each level). *) +let rec map_rel_context_lift f env i (ctxt:EConstr.rel_context):EConstr.rel_context = + match ctxt with + | [] -> ctxt + | decl::ctxt' -> f i decl :: map_rel_context_lift f env (i+1) ctxt' + (* Instantiating some arguments (whatever their position) of an hypothesis or any term, leaving other arguments quantified. If operating on an hypothesis of the goal, the new hypothesis replaces it. @@ -2993,16 +3000,17 @@ let quantify lconstr = solve, ui are a mix of inferred args and yi. The overall effect is to remove from H as much quantification as possible given lbind. *) + let specialize (c,lbind) ipat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, term = + let typ_of_c = Retyping.get_type_of env sigma c in + let sigma, term, typ = if lbind == NoBindings then - sigma, c + sigma, c, typ_of_c else (* ***** SOLVING ARGS ******* *) - let typ_of_c = Retyping.get_type_of env sigma c in (* If the term is lambda then we put a letin to put avoid interaction between the term and the bindings. *) let c = match EConstr.kind sigma c with @@ -3028,38 +3036,53 @@ let specialize (c,lbind) ipat = | _ -> x in (* We grab names used in product to remember them at re-abstracting phase *) let typ_of_c_hd = pf_get_type_of gl thd in - let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in + let (lprod:rel_context), concl = decompose_prod_assum sigma typ_of_c_hd in (* lprd = initial products (including letins). l(tstack initially) = the same products after unification vs lbind (some metas remain) args: accumulator : args to apply to hd: inferred args + metas reabstracted *) - let rec rebuild_lambdas sigma lprd args hd l = + let rec rebuild sigma concl (lprd:rel_context) (accargs:EConstr.t list) + (accprods:rel_context) hd (l:EConstr.t list) = + let open Context.Rel.Declaration in match lprd , l with - | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) - | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> + | _, [] -> sigma + , applist (hd, (List.map (nf_evar sigma) (List.rev accargs))) + , EConstr.it_mkProd_or_LetIn concl accprods + | (LocalAssum(nme,_) as assum)::lp' , t::l' when occur_meta sigma t -> (* nme has not been resolved, let us re-abstract it. Same name but type updated by instantiation of other args. *) let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in let r = Retyping.relevance_of_type env sigma new_typ_of_t in - let liftedargs = List.map liftrel args in (* lifting rels in the accumulator args *) - let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in + let liftedargs = List.map liftrel accargs in + let sigma,hd',prods = + rebuild sigma concl lp' (mkRel 1 ::liftedargs) (assum::accprods) hd l' in (* replace meta variable by the abstracted variable *) let hd'' = subst_term sigma t hd' in - (* lambda expansion *) - sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd'') - | Context.Rel.Declaration.LocalAssum _::lp' , t::l' -> - let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in - sigma,hd' - | Context.Rel.Declaration.LocalDef _::lp' , _ -> - (* letins have been reduced in l and should anyway not - correspond to an arg, we ignore them. *) - let sigma,hd' = rebuild_lambdas sigma lp' args hd l in - sigma,hd' + (* we reabstract the non solved argument *) + sigma,mkLambda ({nme with binder_relevance=r},new_typ_of_t,hd''),prods + | (LocalAssum (nme,tnme))::lp' , t::l' -> + (* thie arg was solved, we update thing accordingly *) + (* we replace in lprod the arg by rel 1 *) + let substlp' = (* rel 1 must be lifted along the context *) + map_rel_context_lift (fun i x -> map_constr (replace_term sigma (mkRel i) t) x) + env 1 lp' in + (* Then we lift every rel above the just removed arg *) + let updatedlp' = + map_rel_context_lift (fun i x -> map_constr (liftn (-1) i) x) env 1 substlp' in + (* We replace also the term in the conclusion, its rel index is the + length of the list lprd (remaining products before concl) *) + let concl'' = replace_term sigma (mkRel (List.length lprd)) t concl in + (* we also lift in concl the index above the arg *) + let concl' = liftn (-1) (List.length lprd) concl'' in + rebuild sigma concl' updatedlp' (t::accargs) accprods hd l' + | LocalDef _ as assum::lp' , _ -> + (* letins have been reduced in l and should anyway not correspond to an arg, we + ignore them, but we remember them in accprod, so that they remain in the type. *) + rebuild sigma concl lp' accargs (assum::accprods) hd l | _ ,_ -> assert false in - let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] thd tstack in - Evd.clear_metas sigma, hd + let sigma,hd,newtype = rebuild sigma concl (List.rev lprod) [] [] thd tstack in + Evd.clear_metas sigma, hd, newtype in - let typ = Retyping.get_type_of env sigma term in let tac = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> diff --git a/test-suite/Makefile b/test-suite/Makefile index 1d21b4b5e0..265c2eafa7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -643,7 +643,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @echo "TEST $<" $(HIDE){ \ - $(coqc) -quick -R vio vio $* 2>&1 && \ + $(coqc) -vio -R vio vio $* 2>&1 && \ $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \ $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v new file mode 100644 index 0000000000..87f15a4a19 --- /dev/null +++ b/test-suite/bugs/closed/bug_11133.v @@ -0,0 +1,18 @@ +Module Type Universe. +Parameter U : nat. +End Universe. + +Module Univ_prop (Univ : Universe). +Include Univ. +End Univ_prop. + +Module Monad (Univ : Universe). +Module UP := (Univ_prop Univ). +End Monad. + +Module Rules (Univ:Universe). +Module MP := Monad Univ. +Include MP. +Import UP. +Definition M := UP.U. (* anomaly here *) +End Rules. diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v new file mode 100644 index 0000000000..6e109e33e6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11168.v @@ -0,0 +1,5 @@ +Axiom f : forall T, T. +Arguments f &. +Check f _ _. +Check f (_ -> _) _. +Check f (forall x, _) _. diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v new file mode 100644 index 0000000000..8ddf05c888 --- /dev/null +++ b/test-suite/bugs/closed/bug_11421.v @@ -0,0 +1 @@ +Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}. diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v index ff08bdc6bb..52cc34beb3 100644 --- a/test-suite/bugs/closed/bug_2729.v +++ b/test-suite/bugs/closed/bug_2729.v @@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Arguments Nil [pu cxt]. +Arguments Nil {pu cxt}. Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 298a07c1c4..7022987096 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Arguments ADMIT [p]. +Arguments ADMIT {p}. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out new file mode 100644 index 0000000000..0b4b4b6e37 --- /dev/null +++ b/test-suite/coqdoc/bug11353.html.out @@ -0,0 +1,39 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug11353</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug11353</h1> + +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> +<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> + | <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a><br/> + | <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a>.<br/> + +<br/> +#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out new file mode 100644 index 0000000000..a6478682d8 --- /dev/null +++ b/test-suite/coqdoc/bug11353.tex.out @@ -0,0 +1,34 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug11353}{Library }{Coqdoc.bug11353} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[ \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol +\coqdocnoindent +\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug11353.v b/test-suite/coqdoc/bug11353.v new file mode 100644 index 0000000000..b68902c8cc --- /dev/null +++ b/test-suite/coqdoc/bug11353.v @@ -0,0 +1,7 @@ +(* -*- coq-prog-args: ("-g") -*- *) +Definition a := 0. #[ (* templatize *) universes( template) ] +Inductive mysum (A B:Type) : Type := + | myinl : A -> mysum A B + | myinr : B -> mysum A B. + +#[local]Definition b := 1. diff --git a/test-suite/micromega/bug_11191a.v b/test-suite/micromega/bug_11191a.v new file mode 100644 index 0000000000..57c1d7d52f --- /dev/null +++ b/test-suite/micromega/bug_11191a.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p n, (0 < Z.pos (p ^ n))%Z. + intros. + lia. +Qed. diff --git a/test-suite/micromega/bug_11191b.v b/test-suite/micromega/bug_11191b.v new file mode 100644 index 0000000000..007470c5b3 --- /dev/null +++ b/test-suite/micromega/bug_11191b.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p, (0 < Z.pos (p ^ 2))%Z. + intros. + lia. +Qed. diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh index 96bdee2fc2..e60fb48bca 100755 --- a/test-suite/misc/quick-include.sh +++ b/test-suite/misc/quick-include.sh @@ -1,5 +1,5 @@ #!/bin/sh set -e -$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v -$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v +$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v +$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index b2e3c3e923..fbb3c6bdab 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) Module M. Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 505c5ce378..a961330b81 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) Section S. Definition foo := nonexistent. End S. diff --git a/test-suite/output/ExtractionString.out b/test-suite/output/ExtractionString.out new file mode 100644 index 0000000000..2a101d9cea --- /dev/null +++ b/test-suite/output/ExtractionString.out @@ -0,0 +1,52 @@ +(** val str : string **) + +let str = + String ((Ascii (False, False, True, False, True, False, True, False)), + (String ((Ascii (False, False, False, True, False, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, False, False, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, True, False, True, True, True, False)), + (String ((Ascii (False, True, False, False, True, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (False, True, True, True, False, True, True, False)), + (String ((Ascii (True, True, True, False, False, True, True, False)), + EmptyString))))))))))))))))))))))))))))))) +str :: String +str = + String0 (Ascii False False True False True False True False) (String0 + (Ascii False False False True False True True False) (String0 (Ascii True + False False True False True True False) (String0 (Ascii True True False + False True True True False) (String0 (Ascii False False False False False + True False False) (String0 (Ascii True False False True False True True + False) (String0 (Ascii True True False False True True True False) + (String0 (Ascii False False False False False True False False) (String0 + (Ascii True False False False False True True False) (String0 (Ascii + False False False False False True False False) (String0 (Ascii True True + False False True True True False) (String0 (Ascii False False True False + True True True False) (String0 (Ascii False True False False True True + True False) (String0 (Ascii True False False True False True True False) + (String0 (Ascii False True True True False True True False) (String0 + (Ascii True True True False False True True False) + EmptyString))))))))))))))) + + +(** val str : char list **) + +let str = + 'T'::('h'::('i'::('s'::(' '::('i'::('s'::(' '::('a'::(' '::('s'::('t'::('r'::('i'::('n'::('g'::[]))))))))))))))) +(** val str : string **) + +let str = + "This is a string" +str :: Prelude.String +str = + "This is a string" + + diff --git a/test-suite/output/ExtractionString.v b/test-suite/output/ExtractionString.v new file mode 100644 index 0000000000..e4b9d22b38 --- /dev/null +++ b/test-suite/output/ExtractionString.v @@ -0,0 +1,25 @@ +Require Import String Extraction. + +Definition str := "This is a string"%string. + +(* Raw extraction of strings, in OCaml *) +Extraction Language OCaml. +Extraction str. + +(* Raw extraction of strings, in Haskell *) +Extraction Language Haskell. +Extraction str. + +(* Extraction to char list, in OCaml *) +Require Import ExtrOcamlString. +Extraction Language OCaml. +Extraction str. + +(* Extraction to native strings, in OCaml *) +Require Import ExtrOcamlNativeString. +Extraction str. + +(* Extraction to native strings, in Haskell *) +Require Import ExtrHaskellString. +Extraction Language Haskell. +Extraction str. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index d293dc0533..048fb3b027 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -65,7 +65,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Arguments eqP [T x y]. +Arguments eqP {T x y}. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -345,7 +345,7 @@ Proof. by []. Qed. End SubEqType. -Arguments val_eqP [T P sT x y]. +Arguments val_eqP {T P sT x y}. Prenex Implicits val_eqP. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) @@ -386,7 +386,7 @@ Qed. Canonical nat_eqMixin := EqMixin eqnP. Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. -Arguments eqnP [x y]. +Arguments eqnP {x y}. Prenex Implicits eqnP. Coercion nat_of_bool (b : bool) := if b then 1 else 0. diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index e6d674c1e6..88702a6e80 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -51,3 +51,22 @@ Fail Check (refl_equal _ : l _ = x2). Check s0. Check s1. Check s2. + +Section Y. + Let s3 := MKL x3. + Canonical Structure s3. + Check (refl_equal _ : l _ = x3). +End Y. +Fail Check (refl_equal _ : l _ = x3). +Fail Check s3. + +Section V. + #[canonical] Let s3 := MKL x3. + Check (refl_equal _ : l _ = x3). +End V. + +Section W. + #[canonical, local] Definition s2' := MKL x2. + Check (refl_equal _ : l _ = x2). +End W. +Fail Check (refl_equal _ : l _ = x2). diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index c2130995fc..4b2d4457bf 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Arguments LNil [A]. +Arguments LNil {A}. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil @@ -204,3 +204,19 @@ End NonRecLetIn. Fail Inductive foo (T : Type) : let T := Type in T := { r : forall x : T, x = x }. + +Module Discharge. + (* discharge test *) + Section S. + Let x := Prop. + Inductive foo : x := bla : foo. + End S. + Check bla:foo. + + Section S. + Variables (A:Type). + (* ensure params are scanned for needed section variables even with template arity *) + #[universes(template)] Inductive bar (d:A) := . + End S. + Check @bar nat 0. +End Discharge. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 1dbeaf3e1f..8297f54641 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Arguments NL [I]. +Arguments NL {I}. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 4fac798f76..15672eab7c 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -994,7 +994,7 @@ Qed. Arguments Vector.cons [A] _ [n]. -Arguments Vector.nil [A]. +Arguments Vector.nil {A}. Arguments Vector.hd [A n]. Arguments Vector.tl [A n]. @@ -1161,7 +1161,7 @@ infiniteproof map_iterate'. Qed. -Arguments LNil [A]. +Arguments LNil {A}. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 1b04594290..1122b9fa34 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -109,28 +109,37 @@ match goal with H:_ |- _ => clear H end. match goal with H:_ |- _ => exact H end. Qed. -(* let ins should be supported in the type of the specialized hypothesis *) -Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False. + +(* let ins should be supported int he type of the specialized hypothesis *) +Axiom foo: forall (m1:nat) (m2: nat), let n := 2 * m1 in (m1 = m2 -> False). Goal False. pose proof foo as P. assert (2 = 2) as A by reflexivity. + (* specialize P with (m2:= 2). *) specialize P with (1 := A). + match type of P with + | let n := 2 * 2 in False => idtac + | _ => fail "test failed" + end. assumption. Qed. (* Another more subtle test on letins: they should not interfere with foralls. *) -Goal forall (P: forall y:nat, - forall A (zz:A), - let a := zz in - let x := 1 in - forall n : y = x, - n = n), +Goal forall (P: forall a c:nat, + let b := c in + let d := 1 in + forall n : a = d, a = c+1), True. intros P. - specialize P with (zz := @eq_refl _ 2). + specialize P with (1:=eq_refl). + match type of P with + | forall c : nat, let f := c in let d := 1 in 1 = c + 1 => idtac + | _ => fail "test failed" + end. constructor. Qed. + (* Test specialize as *) Goal (forall x, x=0) -> 1=0. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 38723e291f..74335da2f1 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -120,62 +120,6 @@ Section Facts. Qed. - (************************) - (** *** Facts about [In] *) - (************************) - - - (** Characterization of [In] *) - - Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). - Proof. - simpl; auto. - Qed. - - Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). - Proof. - simpl; auto. - Qed. - - Theorem not_in_cons (x a : A) (l : list A): - ~ In x (a::l) <-> x<>a /\ ~ In x l. - Proof. - simpl. intuition. - Qed. - - Theorem in_nil : forall a:A, ~ In a []. - Proof. - unfold not; intros a H; inversion_clear H. - Qed. - - Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. - Proof. - induction l; simpl; destruct 1. - subst a; auto. - exists [], l; auto. - destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1), l2; simpl. apply f_equal. auto. - Qed. - - (** Inversion *) - Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. - Proof. - intros a b l H; inversion_clear H; auto. - Qed. - - (** Decidability of [In] *) - Theorem in_dec : - (forall x y:A, {x = y} + {x <> y}) -> - forall (a:A) (l:list A), {In a l} + {~ In a l}. - Proof. - intro H; induction l as [| a0 l IHl]. - right; apply in_nil. - destruct (H a0 a); simpl; auto. - destruct IHl; simpl; auto. - right; unfold not; intros [Hc1| Hc2]; auto. - Defined. - - (**************************) (** *** Facts about [app] *) (**************************) @@ -255,6 +199,14 @@ Section Facts. apply app_cons_not_nil in H1 as []. Qed. + Lemma elt_eq_unit : forall l1 l2 (a b : A), + l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []. + Proof. + intros l1 l2 a b Heq. + apply app_eq_unit in Heq. + now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2. + Qed. + Lemma app_inj_tail : forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. @@ -281,6 +233,61 @@ Section Facts. induction l; simpl; auto. Qed. + Lemma last_length : forall (l : list A) a, length (l ++ a :: nil) = S (length l). + Proof. + intros ; rewrite app_length ; simpl. + rewrite <- plus_n_Sm, plus_n_O; reflexivity. + Qed. + + Lemma app_inv_head: + forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Proof. + induction l; simpl; auto; injection 1; auto. + Qed. + + Lemma app_inv_tail: + forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Proof. + intros l l1 l2; revert l1 l2 l. + induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; + simpl; auto; intros l H. + absurd (length (x2 :: l2 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite <- H; auto with arith. + absurd (length (x1 :: l1 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite H; auto with arith. + injection H as [= H H0]; f_equal; eauto. + Qed. + + (************************) + (** *** Facts about [In] *) + (************************) + + + (** Characterization of [In] *) + + Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). + Proof. + simpl; auto. + Qed. + + Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). + Proof. + simpl; auto. + Qed. + + Theorem not_in_cons (x a : A) (l : list A): + ~ In x (a::l) <-> x<>a /\ ~ In x l. + Proof. + simpl. intuition. + Qed. + + Theorem in_nil : forall a:A, ~ In a []. + Proof. + unfold not; intros a H; inversion_clear H. + Qed. + Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m. Proof. intros l m a. @@ -314,27 +321,48 @@ Section Facts. split; auto using in_app_or, in_or_app. Qed. - Lemma app_inv_head: - forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. Proof. - induction l; simpl; auto; injection 1; auto. + induction l; simpl; destruct 1. + subst a; auto. + exists [], l; auto. + destruct (IHl H) as (l1,(l2,H0)). + exists (a::l1), l2; simpl. apply f_equal. auto. Qed. - Lemma app_inv_tail: - forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Lemma in_elt : forall (x:A) l1 l2, In x (l1 ++ x :: l2). Proof. - intros l l1 l2; revert l1 l2 l. - induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; - simpl; auto; intros l H. - absurd (length (x2 :: l2 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite <- H; auto with arith. - absurd (length (x1 :: l1 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite H; auto with arith. - injection H as [= H H0]; f_equal; eauto. + intros. + apply in_or_app. + right; left; reflexivity. + Qed. + + Lemma in_elt_inv : forall (x y : A) l1 l2, + In x (l1 ++ y :: l2) -> x = y \/ In x (l1 ++ l2). + Proof. + intros x y l1 l2 Hin. + apply in_app_or in Hin. + destruct Hin as [Hin|[Hin|Hin]]; [right|left|right]; try apply in_or_app; intuition. Qed. + (** Inversion *) + Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. + Proof. easy. Qed. + + (** Decidability of [In] *) + Theorem in_dec : + (forall x y:A, {x = y} + {x <> y}) -> + forall (a:A) (l:list A), {In a l} + {~ In a l}. + Proof. + intro H; induction l as [| a0 l IHl]. + right; apply in_nil. + destruct (H a0 a); simpl; auto. + destruct IHl; simpl; auto. + right; unfold not; intros [Hc1| Hc2]; auto. + Defined. + + + End Facts. Hint Resolve app_assoc app_assoc_reverse: datatypes. @@ -463,6 +491,22 @@ Section Elts. - intros; simpl; rewrite IHl; auto with arith. Qed. + Lemma app_nth2_plus : forall l l' d n, + nth (length l + n) (l ++ l') d = nth n l' d. + Proof. + intros. + rewrite app_nth2, minus_plus; trivial. + auto with arith. + Qed. + + Lemma nth_middle : forall l l' a d, + nth (length l) (l ++ a :: l') d = a. + Proof. + intros. + rewrite plus_n_O at 1. + apply app_nth2_plus. + Qed. + Lemma nth_split n l d : n < length l -> exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n. Proof. @@ -473,6 +517,20 @@ Section Elts. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. + Lemma nth_ext : forall l l' d, length l = length l' -> + (forall n, nth n l d = nth n l' d) -> l = l'. + Proof. + induction l; intros l' d Hlen Hnth; destruct l' as [| b l']. + - reflexivity. + - inversion Hlen. + - inversion Hlen. + - change a with (nth 0 (a :: l) d). + change b with (nth 0 (b :: l') d). + rewrite Hnth; f_equal. + apply IHl with d; [ now inversion Hlen | ]. + intros n; apply (Hnth (S n)). + Qed. + (** Results about [nth_error] *) Lemma nth_error_In l n x : nth_error l n = Some x -> In x l. @@ -556,31 +614,9 @@ Section Elts. rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity. Qed. - (*****************) - (** ** Remove *) - (*****************) - - Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - - Fixpoint remove (x : A) (l : list A) : list A := - match l with - | [] => [] - | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) - end. - - Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). - Proof. - induction l as [|x l]; auto. - intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. - apply IHl. - unfold not; intro HF; simpl in HF; destruct HF; auto. - apply (IHl y); assumption. - Qed. - - -(******************************) -(** ** Last element of a list *) -(******************************) + (******************************) + (** ** Last element of a list *) + (******************************) (** [last l d] returns the last element of the list [l], or the default value [d] if [l] is empty. *) @@ -592,6 +628,13 @@ Section Elts. | a :: l => last l d end. + Lemma last_last : forall l a d, last (l ++ [a]) d = a. + Proof. + induction l; intros; [ reflexivity | ]. + simpl; rewrite IHl. + destruct l; reflexivity. + Qed. + (** [removelast l] remove the last element of [l] *) Fixpoint removelast (l:list A) : list A := @@ -638,6 +681,119 @@ Section Elts. destruct (l++l'); [elim H0; auto|f_equal; auto]. Qed. + Lemma removelast_last : forall l a, removelast (l ++ [a]) = l. + Proof. + intros. + rewrite removelast_app. + - apply app_nil_r. + - intros Heq; inversion Heq. + Qed. + + + (*****************) + (** ** Remove *) + (*****************) + + Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + + Fixpoint remove (x : A) (l : list A) : list A := + match l with + | [] => [] + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + end. + + Lemma remove_cons : forall x l, remove x (x :: l) = remove x l. + Proof. + intros x l; simpl; destruct (eq_dec x x); [ reflexivity | now exfalso ]. + Qed. + + Lemma remove_app : forall x l1 l2, + remove x (l1 ++ l2) = remove x l1 ++ remove x l2. + Proof. + induction l1; intros l2; simpl. + - reflexivity. + - destruct (eq_dec x a). + + apply IHl1. + + rewrite <- app_comm_cons; f_equal. + apply IHl1. + Qed. + + Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). + Proof. + induction l as [|x l]; auto. + intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. + apply IHl. + unfold not; intro HF; simpl in HF; destruct HF; auto. + apply (IHl y); assumption. + Qed. + + Lemma notin_remove: forall l x, ~ In x l -> remove x l = l. + Proof. + intros l x; induction l as [|y l]; simpl; intros Hnin. + - reflexivity. + - destruct (eq_dec x y); subst; intuition. + f_equal; assumption. + Qed. + + Lemma in_remove: forall l x y, In x (remove y l) -> In x l /\ x <> y. + Proof. + induction l as [|z l]; intros x y Hin. + - inversion Hin. + - simpl in Hin. + destruct (eq_dec y z) as [Heq|Hneq]; subst; split. + + right; now apply IHl with z. + + intros Heq; revert Hin; subst; apply remove_In. + + inversion Hin; subst; [left; reflexivity|right]. + now apply IHl with y. + + destruct Hin as [Hin|Hin]; subst. + * now intros Heq; apply Hneq. + * intros Heq; revert Hin; subst; apply remove_In. + Qed. + + Lemma in_in_remove : forall l x y, x <> y -> In x l -> In x (remove y l). + Proof. + induction l as [|z l]; simpl; intros x y Hneq Hin. + - apply Hin. + - destruct (eq_dec y z); subst. + + destruct Hin. + * exfalso; now apply Hneq. + * now apply IHl. + + simpl; destruct Hin; [now left|right]. + now apply IHl. + Qed. + + Lemma remove_remove_comm : forall l x y, + remove x (remove y l) = remove y (remove x l). + Proof. + induction l as [| z l]; simpl; intros x y. + - reflexivity. + - destruct (eq_dec y z); simpl; destruct (eq_dec x z); try rewrite IHl; auto. + + subst; symmetry; apply remove_cons. + + simpl; destruct (eq_dec y z); tauto. + Qed. + + Lemma remove_remove_eq : forall l x, remove x (remove x l) = remove x l. + Proof. intros l x; now rewrite (notin_remove _ _ (remove_In l x)). Qed. + + Lemma remove_length_le : forall l x, length (remove x l) <= length l. + Proof. + induction l as [|y l IHl]; simpl; intros x; trivial. + destruct (eq_dec x y); simpl. + - rewrite IHl; constructor; reflexivity. + - apply (proj1 (Nat.succ_le_mono _ _) (IHl x)). + Qed. + + Lemma remove_length_lt : forall l x, In x l -> length (remove x l) < length l. + Proof. + induction l as [|y l IHl]; simpl; intros x Hin. + - contradiction Hin. + - destruct Hin as [-> | Hin]. + + destruct (eq_dec x x); intuition. + apply Nat.lt_succ_r, remove_length_le. + + specialize (IHl _ Hin); destruct (eq_dec x y); simpl; auto. + now apply Nat.succ_lt_mono in IHl. + Qed. + (******************************************) (** ** Counting occurrences of an element *) @@ -743,6 +899,12 @@ Section ListOps. rewrite IHl; auto. Qed. + Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1. + Proof. + intros l l1 l2 Heq. + rewrite <- (rev_involutive l), Heq. + apply rev_app_distr. + Qed. (** Compatibility with other operations *) @@ -820,30 +982,27 @@ Section ListOps. Section Reverse_Induction. - Lemma rev_list_ind : - forall P:list A-> Prop, - P [] -> - (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> - forall l:list A, P (rev l). + Lemma rev_list_ind : forall P:list A-> Prop, + P [] -> + (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> + forall l:list A, P (rev l). Proof. induction l; auto. Qed. - Theorem rev_ind : - forall P:list A -> Prop, - P [] -> - (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. + Theorem rev_ind : forall P:list A -> Prop, + P [] -> + (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. Proof. intros. generalize (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind P). - auto. - - simpl. - intros. - apply (H0 a (rev l0)). - auto. + - auto. + - simpl. + intros. + apply (H0 a (rev l0)). + auto. Qed. End Reverse_Induction. @@ -871,10 +1030,28 @@ Section ListOps. Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2. Proof. intros l1; induction l1 as [|x l1 IH]; intros l2; simpl. - + reflexivity. - + rewrite IH; apply app_assoc. + - reflexivity. + - rewrite IH; apply app_assoc. Qed. + Lemma in_concat : forall l y, + In y (concat l) <-> exists x, In x l /\ In y x. + Proof. + induction l; simpl; split; intros. + contradiction. + destruct H as (x,(H,_)); contradiction. + destruct (in_app_or _ _ _ H). + exists a; auto. + destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). + exists x; auto. + apply in_or_app. + destruct H as (x,(H0,H1)); destruct H0. + subst; auto. + right; destruct (IHl y) as (_,H2); apply H2. + exists x; auto. + Qed. + + (***********************************) (** ** Decidable equality on lists *) (***********************************) @@ -944,6 +1121,13 @@ Section Map. intros; rewrite IHl; auto. Qed. + Lemma map_last : forall l a, + map (l ++ [a]) = (map l) ++ [f a]. + Proof. + induction l; intros; [ reflexivity | ]. + simpl; rewrite IHl; reflexivity. + Qed. + Lemma map_rev : forall l, map (rev l) = rev (map l). Proof. induction l; simpl; auto. @@ -956,6 +1140,26 @@ Section Map. destruct l; simpl; reflexivity || discriminate. Qed. + Lemma map_eq_cons : forall l l' b, + map l = b :: l' -> exists a tl, l = a :: tl /\ b = f a /\ l' = map tl. + Proof. + intros l l' b Heq. + destruct l; inversion_clear Heq. + exists a, l; repeat split. + Qed. + + Lemma map_eq_app : forall l l1 l2, + map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ l1 = map l1' /\ l2 = map l2'. + Proof. + induction l; simpl; intros l1 l2 Heq. + - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. + exists nil, nil; repeat split. + - destruct l1; simpl in Heq; inversion Heq as [[Heq2 Htl]]. + + exists nil, (a :: l); repeat split. + + destruct (IHl _ _ Htl) as (l1' & l2' & ? & ? & ?); subst. + exists (a :: l1'), l2'; repeat split. + Qed. + (** [map] and count of occurrences *) Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}. @@ -969,10 +1173,10 @@ Section Map. - reflexivity. - specialize (Hrec x). destruct (decA a x) as [H1|H1], (decB (f a) (f x)) as [H2|H2]. - * rewrite Hrec. reflexivity. - * contradiction H2. rewrite H1. reflexivity. - * specialize (Hfinjective H2). contradiction H1. - * assumption. + + rewrite Hrec. reflexivity. + + contradiction H2. rewrite H1. reflexivity. + + specialize (Hfinjective H2). contradiction H1. + + assumption. Qed. (** [flat_map] *) @@ -984,10 +1188,18 @@ Section Map. | cons x t => (f x)++(flat_map t) end. + Lemma flat_map_app : forall f l1 l2, + flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2. + Proof. + intros F l1 l2. + induction l1; [ reflexivity | simpl ]. + rewrite IHl1, app_assoc; reflexivity. + Qed. + Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), In y (flat_map f l) <-> exists x, In x l /\ In y (f x). - Proof using A B. - clear Hfinjective. + Proof. + clear f Hfinjective. induction l; simpl; split; intros. contradiction. destruct H as (x,(H,_)); contradiction. @@ -1008,15 +1220,22 @@ Lemma flat_map_concat_map : forall A B (f : A -> list B) l, flat_map f l = concat (map f l). Proof. intros A B f l; induction l as [|x l IH]; simpl. -+ reflexivity. -+ rewrite IH; reflexivity. +- reflexivity. +- rewrite IH; reflexivity. Qed. Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). Proof. intros A B f l; induction l as [|x l IH]; simpl. -+ reflexivity. -+ rewrite map_app, IH; reflexivity. +- reflexivity. +- rewrite map_app, IH; reflexivity. +Qed. + +Lemma remove_concat A (eq_dec : forall x y : A, {x = y}+{x <> y}) : forall l x, + remove eq_dec x (concat l) = flat_map (remove eq_dec x) l. +Proof. + intros l x; induction l; [ reflexivity | simpl ]. + rewrite remove_app, IHl; reflexivity. Qed. Lemma map_id : forall (A :Type) (l : list A), @@ -1057,6 +1276,25 @@ Proof. intros; apply map_ext_in; auto. Qed. +Lemma flat_map_ext : forall (A B : Type)(f g : A -> list B), + (forall a, f a = g a) -> forall l, flat_map f l = flat_map g l. +Proof. + intros A B f g Hext l. + rewrite 2 flat_map_concat_map. + now rewrite map_ext with (g := g). +Qed. + +Lemma nth_nth_nth_map A : forall (l : list A) n d ln dn, n < length ln \/ length l <= dn -> + nth (nth n ln dn) l d = nth n (map (fun x => nth x l d) ln) d. +Proof. + intros l n d ln dn; revert n; induction ln; intros n Hlen. + - destruct Hlen as [Hlen|Hlen]. + + inversion Hlen. + + now rewrite nth_overflow; destruct n. + - destruct n; simpl; [ reflexivity | apply IHln ]. + destruct Hlen; [ left; apply lt_S_n | right ]; assumption. +Qed. + (************************************) (** Left-to-right iterator on lists *) @@ -1168,8 +1406,8 @@ End Fold_Right_Recursor. Fixpoint existsb (l:list A) : bool := match l with - | nil => false - | a::l => f a || existsb l + | nil => false + | a::l => f a || existsb l end. Lemma existsb_exists : @@ -1208,8 +1446,8 @@ End Fold_Right_Recursor. Fixpoint forallb (l:list A) : bool := match l with - | nil => true - | a::l => f a && forallb l + | nil => true + | a::l => f a && forallb l end. Lemma forallb_forall : @@ -1231,12 +1469,13 @@ End Fold_Right_Recursor. solve[auto]. case (f a); simpl; solve[auto]. Qed. + (** [filter] *) Fixpoint filter (l:list A) : list A := match l with - | nil => nil - | x :: l => if f x then x::(filter l) else filter l + | nil => nil + | x :: l => if f x then x::(filter l) else filter l end. Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true. @@ -1265,8 +1504,8 @@ End Fold_Right_Recursor. Fixpoint find (l:list A) : option A := match l with - | nil => None - | x :: tl => if f x then Some x else find tl + | nil => None + | x :: tl => if f x then Some x else find tl end. Lemma find_some l x : find l = Some x -> In x l /\ f x = true. @@ -1288,9 +1527,9 @@ End Fold_Right_Recursor. Fixpoint partition (l:list A) : list A * list A := match l with - | nil => (nil, nil) - | x :: tl => let (g,d) := partition tl in - if f x then (x::g,d) else (g,x::d) + | nil => (nil, nil) + | x :: tl => let (g,d) := partition tl in + if f x then (x::g,d) else (g,x::d) end. Theorem partition_cons1 a l l1 l2: @@ -1405,8 +1644,8 @@ End Fold_Right_Recursor. Fixpoint split (l:list (A*B)) : list A * list B := match l with - | [] => ([], []) - | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) + | [] => ([], []) + | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) end. Lemma in_split_l : forall (l:list (A*B))(p:A*B), @@ -1460,8 +1699,8 @@ End Fold_Right_Recursor. Fixpoint combine (l : list A) (l' : list B) : list (A*B) := match l,l' with - | x::tl, y::tl' => (x,y)::(combine tl tl') - | _, _ => nil + | x::tl, y::tl' => (x,y)::(combine tl tl') + | _, _ => nil end. Lemma split_combine : forall (l: list (A*B)), @@ -1528,8 +1767,8 @@ End Fold_Right_Recursor. Fixpoint list_prod (l:list A) (l':list B) : list (A * B) := match l with - | nil => nil - | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') + | nil => nil + | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') end. Lemma in_prod_aux : @@ -1544,17 +1783,17 @@ End Fold_Right_Recursor. Lemma in_prod : forall (l:list A) (l':list B) (x:A) (y:B), - In x l -> In y l' -> In (x, y) (list_prod l l'). + In x l -> In y l' -> In (x, y) (list_prod l l'). Proof. induction l; - [ simpl; tauto - | simpl; intros; apply in_or_app; destruct H; - [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. + [ simpl; tauto + | simpl; intros; apply in_or_app; destruct H; + [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. Lemma in_prod_iff : forall (l:list A)(l':list B)(x:A)(y:B), - In (x,y) (list_prod l l') <-> In x l /\ In y l'. + In (x,y) (list_prod l l') <-> In x l /\ In y l'. Proof. split; [ | intros; apply in_prod; intuition ]. induction l; simpl; intros. @@ -1650,6 +1889,18 @@ Section SetIncl. Definition incl (l m:list A) := forall a:A, In a l -> In a m. Hint Unfold incl : core. + Lemma incl_nil_l : forall l, incl nil l. + Proof. + intros l a Hin; inversion Hin. + Qed. + + Lemma incl_l_nil : forall l, incl l nil -> l = nil. + Proof. + destruct l; intros Hincl. + - reflexivity. + - exfalso; apply Hincl with a; simpl; auto. + Qed. + Lemma incl_refl : forall l:list A, incl l l. Proof. auto. @@ -1694,6 +1945,13 @@ Section SetIncl. Qed. Hint Resolve incl_cons : core. + Lemma incl_cons_inv : forall (a:A) (l m:list A), + incl (a :: l) m -> In a m /\ incl l m. + Proof. + intros a l m Hi. + split; [ | intros ? ? ]; apply Hi; simpl; auto. + Qed. + Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. unfold incl; simpl; intros l m n H H0 a H1. @@ -1702,6 +1960,34 @@ Section SetIncl. Qed. Hint Resolve incl_app : core. + Lemma incl_app_app : forall l1 l2 m1 m2:list A, + incl l1 m1 -> incl l2 m2 -> incl (l1 ++ l2) (m1 ++ m2). + Proof. + intros. + apply incl_app; [ apply incl_appl | apply incl_appr]; assumption. + Qed. + + Lemma incl_app_inv : forall l1 l2 m : list A, + incl (l1 ++ l2) m -> incl l1 m /\ incl l2 m. + Proof. + induction l1; intros l2 m Hin; split; auto. + - apply incl_nil_l. + - intros b Hb; inversion_clear Hb; subst; apply Hin. + + now constructor. + + simpl; apply in_cons. + apply incl_appl with l1; [ apply incl_refl | assumption ]. + - apply IHl1. + now apply incl_cons_inv in Hin. + Qed. + + Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x, + incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2). + Proof. + intros l1 l2 x Hincl y Hin. + apply in_remove in Hin; destruct Hin as [Hin Hneq]. + apply in_in_remove; intuition. + Qed. + End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons @@ -1825,9 +2111,11 @@ Section Cutting. Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l. Proof. reflexivity. Qed. - Lemma skipn_none : forall l, skipn (length l) l = []. + Lemma skipn_all : forall l, skipn (length l) l = nil. Proof. now induction l. Qed. +#[deprecated(since="8.12",note="Use skipn_all instead.")] Notation skipn_none := skipn_all. + Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = []. Proof. intros l L%Nat.sub_0_le; rewrite <-(firstn_all l) at 1. @@ -1855,9 +2143,6 @@ Section Cutting. - destruct l; simpl; auto. Qed. - Lemma skipn_all l: skipn (length l) l = nil. - Proof. now induction l. Qed. - Lemma skipn_app n : forall l1 l2, skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2). Proof. induction n; auto; intros [|]; simpl; auto. Qed. @@ -1884,7 +2169,7 @@ Section Cutting. intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. - now rewrite L, Nat.sub_0_r, skipn_none. + now rewrite L, Nat.sub_0_r, skipn_all. - replace (length (rev l) - (length (rev l) - x)) with (length (rev l) + x - length (rev l)). rewrite minus_plus. reflexivity. @@ -1911,6 +2196,13 @@ Section Cutting. inversion_clear H0. Qed. + Lemma removelast_firstn_len : forall l, + removelast l = firstn (pred (length l)) l. + Proof. + induction l; [ reflexivity | simpl ]. + destruct l; [ | rewrite IHl ]; reflexivity. + Qed. + Lemma firstn_removelast : forall n l, n < length l -> firstn n (removelast l) = firstn n l. Proof. @@ -2082,6 +2374,16 @@ Section ReDun. + now constructor. Qed. + Lemma NoDup_rev l : NoDup l -> NoDup (rev l). + Proof. + induction l; simpl; intros Hnd; [ constructor | ]. + inversion_clear Hnd as [ | ? ? Hnin Hndl ]. + assert (Add a (rev l) (rev l ++ a :: nil)) as Hadd + by (rewrite <- (app_nil_r (rev l)) at 1; apply Add_app). + apply NoDup_Add in Hadd; apply Hadd; intuition. + now apply Hnin, in_rev. + Qed. + (** Effective computation of a list without duplicates *) Hypothesis decA: forall x y : A, {x = y} + {x <> y}. @@ -2110,6 +2412,11 @@ Section ReDun. * reflexivity. Qed. + Lemma nodup_incl l1 l2 : incl l1 (nodup l2) <-> incl l1 l2. + Proof. + split; intros Hincl a Ha; apply nodup_In; intuition. + Qed. + Lemma NoDup_nodup l: NoDup (nodup l). Proof. induction l as [|a l' Hrec]; simpl. @@ -2252,6 +2559,11 @@ Section NatSeq. | S len => start :: seq (S start) len end. + Lemma cons_seq : forall len start, start :: seq (S start) len = seq start (S len). + Proof. + reflexivity. + Qed. + Lemma seq_length : forall len start, length (seq start len) = len. Proof. induction len; simpl; auto. @@ -2284,8 +2596,8 @@ Section NatSeq. - rewrite <- plus_n_O. split;[easy|]. intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - rewrite IHlen, <- plus_n_Sm; simpl; split. - * intros [H|H]; subst; intuition auto with arith. - * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. + + intros [H|H]; subst; intuition auto with arith. + + intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. Qed. Lemma seq_NoDup len start : NoDup (seq start len). @@ -2302,6 +2614,14 @@ Section NatSeq. - now rewrite Nat.add_succ_r, IHlen. Qed. + Lemma seq_S : forall len start, seq start (S len) = seq start len ++ [start + len]. + Proof. + intros len start. + change [start + len] with (seq (start + len) 1). + rewrite <- seq_app. + rewrite <- plus_n_Sm, <- plus_n_O; reflexivity. + Qed. + End NatSeq. Section Exists_Forall. @@ -2328,6 +2648,21 @@ Section Exists_Forall. - induction l; firstorder; subst; auto. Qed. + Lemma Exists_nth l : + Exists l <-> exists i d, i < length l /\ P (nth i l d). + Proof. + split. + - intros HE; apply Exists_exists in HE. + destruct HE as [a [Hin HP]]. + apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + rewrite <- Heq in HP. + now exists i; exists a. + - intros [i [d [Hl HP]]]. + apply Exists_exists; exists (nth i l d); split. + apply nth_In; assumption. + assumption. + Qed. + Lemma Exists_nil : Exists nil <-> False. Proof. split; inversion 1. Qed. @@ -2335,6 +2670,21 @@ Section Exists_Forall. Exists (x::l) <-> P x \/ Exists l. Proof. split; inversion 1; auto. Qed. + Lemma Exists_app l1 l2 : + Exists (l1 ++ l2) <-> Exists l1 \/ Exists l2. + Proof. + induction l1; simpl; split; intros HE; try now intuition. + - inversion_clear HE; intuition. + - destruct HE as [HE|HE]; intuition. + inversion_clear HE; intuition. + Qed. + + Lemma Exists_rev l : Exists l -> Exists (rev l). + Proof. + induction l; intros HE; intuition. + inversion_clear HE; simpl; apply Exists_app; intuition. + Qed. + Lemma Exists_dec l: (forall x:A, {P x} + { ~ P x }) -> {Exists l} + {~ Exists l}. @@ -2342,12 +2692,25 @@ Section Exists_Forall. intro Pdec. induction l as [|a l' Hrec]. - right. abstract now rewrite Exists_nil. - destruct Hrec as [Hl'|Hl']. - * left. now apply Exists_cons_tl. - * destruct (Pdec a) as [Ha|Ha]. - + left. now apply Exists_cons_hd. - + right. abstract now inversion 1. + + left. now apply Exists_cons_tl. + + destruct (Pdec a) as [Ha|Ha]. + * left. now apply Exists_cons_hd. + * right. abstract now inversion 1. Defined. + Lemma Exists_fold_right l : + Exists l <-> fold_right (fun x => or (P x)) False l. + Proof. + induction l; simpl; split; intros HE; try now inversion HE; intuition. + Qed. + + Lemma incl_Exists l1 l2 : incl l1 l2 -> Exists l1 -> Exists l2. + Proof. + intros Hincl HE. + apply Exists_exists in HE; destruct HE as [a [Hin HP]]. + apply Exists_exists; exists a; intuition. + Qed. + Inductive Forall : list A -> Prop := | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). @@ -2362,11 +2725,49 @@ Section Exists_Forall. - induction l; firstorder. Qed. + Lemma Forall_nth l : + Forall l <-> forall i d, i < length l -> P (nth i l d). + Proof. + split. + - intros HF i d Hl. + apply Forall_forall with (x := nth i l d) in HF. + assumption. + apply nth_In; assumption. + - intros HF. + apply Forall_forall; intros a Hin. + apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + rewrite <- Heq; intuition. + Qed. + Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a. Proof. intros; inversion H; trivial. Qed. + Theorem Forall_inv_tail : forall (a:A) l, Forall (a :: l) -> Forall l. + Proof. + intros; inversion H; trivial. + Qed. + + Lemma Forall_app l1 l2 : + Forall (l1 ++ l2) <-> Forall l1 /\ Forall l2. + Proof. + induction l1; simpl; split; intros HF; try now intuition. + - inversion_clear HF; intuition. + - destruct HF as [HF1 HF2]; inversion HF1; intuition. + Qed. + + Lemma Forall_elt a l1 l2 : Forall (l1 ++ a :: l2) -> P a. + Proof. + intros HF; apply Forall_app in HF; destruct HF as [HF1 HF2]; now inversion HF2. + Qed. + + Lemma Forall_rev l : Forall l -> Forall (rev l). + Proof. + induction l; intros HF; intuition. + inversion_clear HF; simpl; apply Forall_app; intuition. + Qed. + Lemma Forall_rect : forall (Q : list A -> Type), Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l. Proof. @@ -2386,53 +2787,89 @@ Section Exists_Forall. + right. abstract now inversion 1. Defined. + Lemma Forall_fold_right l : + Forall l <-> fold_right (fun x => and (P x)) True l. + Proof. + induction l; simpl; split; intros HF; try now inversion HF; intuition. + Qed. + + Lemma incl_Forall l1 l2 : incl l2 l1 -> Forall l1 -> Forall l2. + Proof. + intros Hincl HF. + apply Forall_forall; intros a Ha. + apply Forall_forall with (x:=a) in HF; intuition. + Qed. + End One_predicate. - Theorem Forall_inv_tail - : forall (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs. + Lemma map_ext_Forall B : forall (f g : A -> B) l, + Forall (fun x => f x = g x) l -> map f l = map g l. Proof. - intros P x0 xs H. - apply Forall_forall with (l := xs). - assert (H0 : forall x : A, In x (x0 :: xs) -> P x). - apply Forall_forall with (P := P) (l := x0 :: xs). - exact H. - assert (H1 : forall (x : A) (H2 : In x xs), P x). - intros x H2. - apply (H0 x). - right. - exact H2. - intros x H2. - apply (H1 x H2). + intros; apply map_ext_in, Forall_forall; assumption. Qed. - Theorem Exists_impl - : forall (P Q : A -> Prop), (forall x : A, P x -> Q x) -> forall xs : list A, Exists P xs -> Exists Q xs. + Theorem Exists_impl : forall (P Q : A -> Prop), (forall a : A, P a -> Q a) -> + forall l, Exists P l -> Exists Q l. Proof. - intros P Q H xs H0. + intros P Q H l H0. induction H0. apply (Exists_cons_hd Q x l (H x H0)). apply (Exists_cons_tl x IHExists). Qed. + Lemma Exists_or : forall (P Q : A -> Prop) l, + Exists P l \/ Exists Q l -> Exists (fun x => P x \/ Q x) l. + Proof. + induction l; intros [H | H]; inversion H; subst. + 1,3: apply Exists_cons_hd; auto. + all: apply Exists_cons_tl, IHl; auto. + Qed. + + Lemma Exists_or_inv : forall (P Q : A -> Prop) l, + Exists (fun x => P x \/ Q x) l -> Exists P l \/ Exists Q l. + Proof. + induction l; intro Hl; inversion Hl as [ ? ? H | ? ? H ]; subst. + - inversion H; now repeat constructor. + - destruct (IHl H); now repeat constructor. + Qed. + + Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall l, Forall P l -> Forall Q l. + Proof. + intros P Q H l. rewrite !Forall_forall. firstorder. + Qed. + + Lemma Forall_and : forall (P Q : A -> Prop) l, + Forall P l -> Forall Q l -> Forall (fun x => P x /\ Q x) l. + Proof. + induction l; intros HP HQ; constructor; inversion HP; inversion HQ; auto. + Qed. + + Lemma Forall_and_inv : forall (P Q : A -> Prop) l, + Forall (fun x => P x /\ Q x) l -> Forall P l /\ Forall Q l. + Proof. + induction l; intro Hl; split; constructor; inversion Hl; firstorder. + Qed. + Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : - Forall (fun x => ~ P x) l <-> ~(Exists P l). + Forall (fun x => ~ P x) l <-> ~(Exists P l). Proof. - rewrite Forall_forall, Exists_exists. firstorder. + rewrite Forall_forall, Exists_exists. firstorder. Qed. Lemma Exists_Forall_neg (P:A->Prop)(l:list A) : (forall x, P x \/ ~P x) -> Exists (fun x => ~ P x) l <-> ~(Forall P l). Proof. - intro Dec. - split. - - rewrite Forall_forall, Exists_exists; firstorder. - - intros NF. - induction l as [|a l IH]. - + destruct NF. constructor. - + destruct (Dec a) as [Ha|Ha]. - * apply Exists_cons_tl, IH. contradict NF. now constructor. - * now apply Exists_cons_hd. + intro Dec. + split. + - rewrite Forall_forall, Exists_exists; firstorder. + - intros NF. + induction l as [|a l IH]. + + destruct NF. constructor. + + destruct (Dec a) as [Ha|Ha]. + * apply Exists_cons_tl, IH. contradict NF. now constructor. + * now apply Exists_cons_hd. Qed. Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) : @@ -2455,17 +2892,61 @@ Section Exists_Forall. now apply neg_Forall_Exists_neg. Defined. - Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> - forall l, Forall P l -> Forall Q l. - Proof. - intros P Q H l. rewrite !Forall_forall. firstorder. - Qed. - End Exists_Forall. Hint Constructors Exists : core. Hint Constructors Forall : core. +Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, + (exists k, Forall (P k) l) -> Forall (fun x => exists k, P k x) l. +Proof. + induction l; intros [k HF]; constructor; inversion_clear HF. + - now exists k. + - now apply IHl; exists k. +Qed. + +Lemma Forall_image A B : forall (f : A -> B) l, + Forall (fun y => exists x, y = f x) l <-> exists l', l = map f l'. +Proof. + induction l; split; intros HF. + - exists nil; reflexivity. + - constructor. + - inversion_clear HF as [| ? ? [x Hx] HFtl]; subst. + destruct (proj1 IHl HFtl) as [l' Heq]; subst. + now exists (x :: l'). + - destruct HF as [l' Heq]. + symmetry in Heq; apply map_eq_cons in Heq. + destruct Heq as (x & tl & ? & ? & ?); subst. + constructor. + + now exists x. + + now apply IHl; exists tl. +Qed. + +Lemma concat_nil_Forall A : forall (l : list (list A)), + concat l = nil <-> Forall (fun x => x = nil) l. +Proof. + induction l; simpl; split; intros Hc; auto. + - apply app_eq_nil in Hc. + constructor; firstorder. + - inversion Hc; subst; simpl. + now apply IHl. +Qed. + +Lemma in_flat_map_Exists A B : forall (f : A -> list B) x l, + In x (flat_map f l) <-> Exists (fun y => In x (f y)) l. +Proof. + intros f x l; rewrite in_flat_map. + split; apply Exists_exists. +Qed. + +Lemma notin_flat_map_Forall A B : forall (f : A -> list B) x l, + ~ In x (flat_map f l) <-> Forall (fun y => ~ In x (f y)) l. +Proof. + intros f x l; rewrite Forall_Exists_neg. + apply not_iff_compat, in_flat_map_Exists. +Qed. + + Section Forall2. (** [Forall2]: stating that elements of two lists are pairwise related. *) @@ -2567,6 +3048,96 @@ Section ForallPairs. Qed. End ForallPairs. +Section Repeat. + + Variable A : Type. + Fixpoint repeat (x : A) (n: nat ) := + match n with + | O => [] + | S k => x::(repeat x k) + end. + + Theorem repeat_length x n: + length (repeat x n) = n. + Proof. + induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. + Qed. + + Theorem repeat_spec n x y: + In y (repeat x n) -> y=x. + Proof. + induction n as [|k Hrec]; simpl; destruct 1; auto. + Qed. + + Lemma repeat_cons n a : + a :: repeat a n = repeat a n ++ (a :: nil). + Proof. + induction n; simpl. + - reflexivity. + - f_equal; apply IHn. + Qed. + +End Repeat. + +Lemma repeat_to_concat A n (a:A) : + repeat a n = concat (repeat [a] n). +Proof. + induction n; simpl. + - reflexivity. + - f_equal; apply IHn. +Qed. + + +(** Sum of elements of a list of [nat]: [list_sum] *) + +Definition list_sum l := fold_right plus 0 l. + +Lemma list_sum_app : forall l1 l2, + list_sum (l1 ++ l2) = list_sum l1 + list_sum l2. +Proof. +induction l1; intros l2; [ reflexivity | ]. +simpl; rewrite IHl1. +apply Nat.add_assoc. +Qed. + +(** Max of elements of a list of [nat]: [list_max] *) + +Definition list_max l := fold_right max 0 l. + +Lemma list_max_app : forall l1 l2, + list_max (l1 ++ l2) = max (list_max l1) (list_max l2). +Proof. +induction l1; intros l2; [ reflexivity | ]. +now simpl; rewrite IHl1, Nat.max_assoc. +Qed. + +Lemma list_max_le : forall l n, + list_max l <= n <-> Forall (fun k => k <= n) l. +Proof. +induction l; simpl; intros n; split; intros H; intuition. +- apply Nat.max_lub_iff in H. + now constructor; [ | apply IHl ]. +- inversion_clear H as [ | ? ? Hle HF ]. + apply IHl in HF; apply Nat.max_lub; assumption. +Qed. + +Lemma list_max_lt : forall l n, l <> nil -> + list_max l < n <-> Forall (fun k => k < n) l. +Proof. +induction l; simpl; intros n Hnil; split; intros H; intuition. +- destruct l. + + repeat constructor. + now simpl in H; rewrite Nat.max_0_r in H. + + apply Nat.max_lub_lt_iff in H. + now constructor; [ | apply IHl ]. +- destruct l; inversion_clear H as [ | ? ? Hlt HF ]. + + now simpl; rewrite Nat.max_0_r. + + apply IHl in HF. + * now apply Nat.max_lub_lt_iff. + * intros Heq; inversion Heq. +Qed. + + (** * Inversion of predicates over lists based on head symbol *) Ltac is_list_constr c := @@ -2633,27 +3204,5 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) Hint Resolve app_nil_end : datatypes. (* end hide *) -Section Repeat. - - Variable A : Type. - Fixpoint repeat (x : A) (n: nat ) := - match n with - | O => [] - | S k => x::(repeat x k) - end. - - Theorem repeat_length x n: - length (repeat x n) = n. - Proof. - induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. - Qed. - - Theorem repeat_spec n x y: - In y (repeat x n) -> y=x. - Proof. - induction n as [|k Hrec]; simpl; destruct 1; auto. - Qed. - -End Repeat. (* Unset Universe Polymorphism. *) diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 28d1c2c97f..332d3b14e4 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -24,7 +24,6 @@ Require Export Rsqrt_def. Require Export R_sqrt. Require Export Rtrigo_calc. Require Export Rgeom. -Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index cb6d57be84..e6b3f2e37b 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -24,7 +24,6 @@ Require Export Rsqrt_def. Require Export R_sqrt. Require Export Rtrigo_calc. Require Export Rgeom. -Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index a848a59d48..0337b12cad 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -15,6 +15,7 @@ Require Import Ranalysis_reg. Require Import Rbase. Require Import RiemannInt_SF. Require Import Max. +Require Import RList. Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 6da0fe3966..c8ec4782d9 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -12,6 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis_reg. Require Import Classical_Prop. +Require Import RList. Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 79ec67b633..6a849bb0b1 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -24,6 +24,9 @@ Declare Scope char_scope. Delimit Scope char_scope with char. Bind Scope char_scope with ascii. +Register ascii as core.ascii.type. +Register Ascii as core.ascii.ascii. + Definition zero := Ascii false false false false false false false false. Definition one := Ascii true false false false false false false false. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 9d0d2f854d..b736f41a08 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -30,8 +30,9 @@ Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. -Register EmptyString as plugins.syntax.EmptyString. -Register String as plugins.syntax.String. +Register string as core.string.type. +Register EmptyString as core.string.empty. +Register String as core.string.string. (** Equality is decidable *) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7cd5962d86..d3ed5e78b4 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -389,7 +389,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles # FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") .PHONY: quick vio2vo: @@ -397,8 +401,9 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +# quick2vo is undocumented quick2vo: - $(HIDE)make -j $(J) quick + $(HIDE)make -j $(J) vio $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ @@ -677,8 +682,8 @@ $(GLOBFILES): %.glob: %.v $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a44ddf7467..13913cabc3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -547,6 +547,9 @@ rule coq_bol = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | space* "#[" { + let eol = begin backtrack lexbuf; body_bol lexbuf end + in if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ @@ -643,6 +646,11 @@ and coq = parse Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | "#[" + { ignore(lexeme lexbuf); + Output.char '#'; Output.char '['; + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } | eof { () } diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 3c198dc600..dceb811d66 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -121,6 +121,10 @@ let compile opts copts ~echo ~f_in ~f_out = in let long_f_dot_in, long_f_dot_out = ensure_exists_with_prefix f_in f_out ext_in ext_out in + let dump_empty_vos () = + (* Produce an empty .vos file, as a way to ensure that a stale .vos can never be loaded *) + let long_f_dot_vos = (chop_extension long_f_dot_out) ^ ".vos" in + create_empty_file long_f_dot_vos in match mode with | BuildVo | BuildVok -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) @@ -145,18 +149,20 @@ let compile opts copts ~echo ~f_in ~f_out = let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - if mode <> BuildVok (* Don't output proofs in -vok mode *) - then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ()); + (* In .vo production, dump a complete .vo file. + In .vok production, only dump an empty .vok file. *) + if mode = BuildVo + then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ()) + else create_empty_file long_f_dot_out; Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); - (* Produce an empty .vos file and an empty .vok file when producing a .vo in standard mode *) + (* In .vo production, dump an empty .vos file to indicate that the .vo should be loaded, + and dump an empty .vok file to indicate that proofs are ok. *) if mode = BuildVo then begin - create_empty_file (long_f_dot_out ^ "s"); + dump_empty_vos(); create_empty_file (long_f_dot_out ^ "k"); end; - (* Produce an empty .vok file when in -vok mode *) - if mode = BuildVok then create_empty_file (long_f_dot_out); Dumpglob.end_dump_glob () | BuildVio | BuildVos -> @@ -186,15 +192,22 @@ let compile opts copts ~echo ~f_in ~f_out = let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let create_vos = (mode = BuildVos) in + (* In .vos production, the output .vos file contains compiled statements. + In .vio production, the output .vio file contains compiled statements and suspended proofs. *) let () = ignore (Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out) in - Stm.reset_task_queue () + Stm.reset_task_queue (); + (* In .vio production, dump an empty .vos file to indicate that the .vio should be loaded. *) + if mode = BuildVio then dump_empty_vos() | Vio2Vo -> let sum, lib, univs, tasks, proofs = Library.load_library_todo long_f_dot_in in let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in - Library.save_library_raw long_f_dot_out sum lib univs proofs + Library.save_library_raw long_f_dot_out sum lib univs proofs; + (* Like in direct .vo production, dump an empty .vok file and an empty .vos file. *) + dump_empty_vos(); + create_empty_file (long_f_dot_out ^ "k") let compile opts copts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5326ce6114..56a6312b61 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -198,6 +198,14 @@ let set_query opts q = | Queries queries -> Queries (queries@[q]) } +let warn_depr_load_ml_object = + CWarnings.create ~name:"deprecated-mlobject" ~category:"deprecated" + (fun () -> Pp.strbrk "The -load-ml-object option is deprecated, see the changelog for more details.") + +let warn_depr_ml_load_source = + CWarnings.create ~name:"deprecated-mlsource" ~category:"deprecated" + (fun () -> Pp.strbrk "The -load-ml-source option is deprecated, see the changelog for more details.") + let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") @@ -396,9 +404,11 @@ let parse_args ~help ~init arglist : t * string list = set_inputstate oval (next ()) |"-load-ml-object" -> + warn_depr_load_ml_object (); Mltop.dir_ml_load (next ()); oval |"-load-ml-source" -> + warn_depr_ml_load_source (); Mltop.dir_ml_use (next ()); oval |"-load-vernac-object" -> diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 178aa362c0..0c15f66c07 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -25,7 +25,6 @@ let coqc_specific_usage = Usage.{ coqc specific options:\ \n -o f.vo use f.vo as the output file name\ \n -verbose compile and output the input file\ -\n -quick quickly compile .v files to .vio files (skip proofs)\ \n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ \n into fi.vo\ \n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ @@ -33,8 +32,10 @@ coqc specific options:\ \n -vos process statements but ignore opaque proofs, and produce a .vos file\ \n -vok process the file by loading .vos instead of .vo files for\ \n dependencies, and produce an empty .vok file on success\ +\n -vio process statements and suspend opaque proofs, and produce a .vio file\ \n\ \nUndocumented:\ +\n -quick (deprecated) alias for -vio\ \n -vio2vo [see manual]\ \n -check-vio-tasks [see manual]\ \n" diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index e614d4fe6d..0c20563d07 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -98,7 +98,7 @@ let set_compilation_mode opts mode = match opts.compilation_mode with | BuildVo -> { opts with compilation_mode = mode } | mode' when mode <> mode' -> - prerr_endline "Options -quick and -vio2vo are exclusive"; + prerr_endline "Options -vio and -vio2vo are exclusive"; exit 1 | _ -> opts @@ -126,6 +126,11 @@ let warn_deprecated_outputstate = (fun () -> Pp.strbrk "The outputstate option is deprecated and discouraged.") +let warn_deprecated_quick = + CWarnings.create ~name:"deprecated-quick" ~category:"deprecated" + (fun () -> + Pp.strbrk "The -quick option is renamed -vio. Please consider using the -vos feature instead.") + let set_outputstate opts s = warn_deprecated_outputstate (); { opts with outputstate = Some s } @@ -165,6 +170,9 @@ let parse arglist : t = | "-o" -> { oval with compilation_output_name = Some (next ()) } | "-quick" -> + warn_deprecated_quick(); + set_compilation_mode oval BuildVio + | "-vio" -> set_compilation_mode oval BuildVio |"-vos" -> Flags.load_vos_libraries := true; diff --git a/vernac/attributes.ml b/vernac/attributes.ml index b7a3b002bd..68d2c3a00d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -234,5 +234,7 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] -let canonical = +let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) +let canonical_instance = + enable_attribute ~key:"canonical" ~default:(fun () -> false) diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 34ff15ca7d..0074db66d3 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -48,7 +48,8 @@ val program : bool attribute val template : bool option attribute val locality : bool option attribute val deprecation : Deprecation.t option attribute -val canonical : bool attribute +val canonical_field : bool attribute +val canonical_instance : bool attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 141b02ef63..e41610b532 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) = let sigma = Evd.from_env env in register_canonical_structure ~warn:true env sigma o -let discharge_canonical_structure (_,(x, local)) = - if local then None else Some (x, local) +let discharge_canonical_structure (_,((gref, _ as x), local)) = + if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None + else Some (x, local) -let inCanonStruc : (Constant.t * inductive) * bool -> obj = + +let inCanonStruc : (GlobRef.t * inductive) * bool -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 69ba9d76ec..def2fdad2a 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -72,7 +72,7 @@ let declare_univ_binders gr pl = CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") + Pp.(str "declare_univ_binders on a constructor reference") in let univs = Id.Map.fold (fun id univ univs -> match Univ.Level.name univ with diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 69ab0fafe9..3302231fd1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram [ [ attr = LIST0 quoted_attributes ; bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; rf_notation = decl_notation -> { - let rf_canonical = attr |> List.flatten |> parse canonical in + let rf_canonical = attr |> List.flatten |> parse canonical_field in let rf_subclass, rf_decl = bd in rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] ; diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index a8462e31e1..506b3bc505 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -138,27 +138,31 @@ let select_vo_file ~warn loadpath base = System.where_in_path ~warn loadpath name in Some (lpath, file) with Not_found -> None in + (* If [!Flags.load_vos_libraries] + and the .vos file exists + and this file is not empty + Then load this library + Else load the most recent between the .vo file and the .vio file, + or if there is only of the two files, take this one, + or raise an error if both are missing. *) + let load_most_recent_of_vo_and_vio () = + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + in if !Flags.load_vos_libraries then begin - (* If the .vos file exists and is not empty, it describes the library. - Otherwise, load the .vo file, or fail if is missing. *) match find ".vos" with | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos - | _ -> - match find ".vo" with - | None -> Error LibNotFound - | Some resvo -> Ok resvo - end else - match find ".vo", find ".vio" with - | None, None -> - Error LibNotFound - | Some res, None | None, Some res -> - Ok res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - Ok resvi - | Some resvo, Some _ -> - Ok resvo + | _ -> load_most_recent_of_vo_and_vio() + end else load_most_recent_of_vo_and_vio() let locate_absolute_library dir : CUnix.physical_path locate_result = (* Search in loadpath *) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8ced35c3be..b999ce9f3f 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -1003,9 +1003,7 @@ let print_canonical_projections env sigma grefs = | Const_cs y -> GlobRef.equal y gr | _ -> false end || - match gr with - | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con - | _ -> false + GlobRef.equal c.o_ORIGIN gr in let projs = List.filter (fun p -> List.for_all (match_proj_gref p) grefs) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4dc883725e..d011fb2e77 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -63,14 +63,15 @@ module DefAttributes = struct polymorphic : bool; program : bool; deprecated : Deprecation.t option; + canonical_instance : bool; } let parse f = let open Attributes in - let ((locality, deprecated), polymorphic), program = - parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f + let (((locality, deprecated), polymorphic), program), canonical_instance = + parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f in - { polymorphic; program; locality; deprecated } + { polymorphic; program; locality; deprecated; canonical_instance } end let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) @@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = in start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl -let vernac_definition_hook ~local ~poly = let open Decls in function +let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> Some (ComCoercion.add_subclass_hook ~poly) +| Definition when canonical_instance -> + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) +| Let when canonical_instance -> + Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None let fresh_name_for_anonymous_theorem () = @@ -551,7 +556,7 @@ let vernac_definition_name lid local = let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in @@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in let scope = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in let program_mode = atts.program in let name = vernac_definition_name lid scope in let red_option = match red_option with |