diff options
58 files changed, 535 insertions, 602 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml deleted file mode 100644 index adab42c622..0000000000 --- a/.circleci/config.yml +++ /dev/null @@ -1,202 +0,0 @@ -# This file used to contain configuration to also build documentation and CoqIDE, -# run the test-suite and the validate targets, -# including with 32-bits architecture or bleeding-edge compiler. - -defaults: - params: ¶ms - # Following parameters are used in Coq CircleCI Job (using yaml - # reference syntax) - working_directory: ~/coq - docker: - - image: $CI_REGISTRY_IMAGE:$CACHEKEY - - environment: &envvars - CACHEKEY: "bionic_coq-V2018-07-11-V2" - CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq - -version: 2 - -before_script: &before_script - name: Setup OPAM Switch - command: | - echo export TERM=xterm >> ~/.profile - source ~/.profile - echo . ~/.profile >> $BASH_ENV - printenv | sort - opam switch "$COMPILER" - opam config list - opam list - -.build-template: &build-template - <<: *params - steps: - - checkout - - run: *before_script - - run: &build-clean - name: Clean - command: | - make clean # ensure that `make clean` works on a fresh clone - - run: &build-configure - name: Configure - command: | - ./configure -local -native-compiler ${NATIVE_COMP} -coqide no - - run: &build-build - name: Build - command: | - make -j ${NJOBS} byte - make -j ${NJOBS} - make test-suite/misc/universes/all_stdlib.v - - persist_to_workspace: - root: &workspace ~/ - paths: - - coq/ - - environment: - <<: *envvars - NATIVE_COMP: "yes" - -.ci-template: &ci-template - <<: *params - steps: - - run: *before_script - - attach_workspace: &attach_workspace - at: *workspace - - - run: - name: Test - command: | - dev/ci/ci-wrapper.sh ${CIRCLE_JOB} - - persist_to_workspace: - root: *workspace - paths: - - coq/ - environment: *envvars - -# Defines individual jobs, see the workflows section below for job orchestration -jobs: - - # Build and prepare test environment - build: *build-template - - bignums: - <<: *ci-template - - color: - <<: *ci-template - - compcert: - <<: *ci-template - - coq-dpdgraph: - <<: *ci-template - - coquelicot: - <<: *ci-template - - cross-crypto: - <<: *ci-template - - elpi: - <<: *ci-template - - equations: - <<: *ci-template - - geocoq: - <<: *ci-template - - fcsl-pcm: - <<: *ci-template - - fiat-crypto: - <<: *ci-template - - fiat-parsers: - <<: *ci-template - - flocq: - <<: *ci-template - - math-classes: - <<: *ci-template - - corn: - <<: *ci-template - - formal-topology: - <<: *ci-template - - hott: - <<: *ci-template - - iris-lambda-rust: - <<: *ci-template - - ltac2: - <<: *ci-template - - math-comp: - <<: *ci-template - - mtac2: - <<: *ci-template - - pidetop: - <<: *ci-template - - sf: - <<: *ci-template - - unimath: - <<: *ci-template - - vst: - <<: *ci-template - -workflows: - version: 2 - - # Run on each push - main: - jobs: - - build - - - bignums: &req-main - requires: - - build - - color: - requires: - - build - - bignums - # - compcert: *req-main - # - coq-dpdgraph: *req-main - # - coquelicot: *req-main - # - cross-crypto: *req-main - # - elpi: *req-main - # - equations: *req-main - # - geocoq: *req-main - # - fcsl-pcm: *req-main - # - fiat-crypto: *req-main - # - fiat-parsers: *req-main - # - flocq: *req-main - - math-classes: - requires: - - build - - bignums - # - mtac2: *req-main - - corn: - requires: - - build - - math-classes - - formal-topology: - requires: - - build - - corn - # - hott: *req-main - # - iris-lambda-rust: *req-main - # - ltac2: *req-main - # - math-comp: *req-main - # - pidetop: *req-main - # - sf: *req-main - # - unimath: *req-main - # - vst: *req-main diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 384e46723a..20d49e675f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -9,7 +9,6 @@ ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers -/.circleci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers @@ -3,7 +3,6 @@ [](https://gitlab.com/coq/coq/commits/master) [](https://travis-ci.org/coq/coq/builds) [](https://ci.appveyor.com/project/coq/coq/branch/master) -[](https://circleci.com/gh/coq/workflows/coq/tree/master) [](https://gitter.im/coq/coq) [](https://doi.org/10.5281/zenodo.1003420) diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index e76a1e9ed8..fd425ef4ff 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -326,10 +326,14 @@ let print_ast fmt ext = end +let declare_plugin fmt name = + fprintf fmt "let %s = \"%s\"@\n" plugin_name name; + fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name + let pr_ast fmt = function | Code s -> fprintf fmt "%s@\n" s.code | Comment s -> fprintf fmt "%s@\n" s -| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name +| DeclarePlugin name -> declare_plugin fmt name | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram | VernacExt -> fprintf fmt "VERNACEXT@\n" | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac diff --git a/dev/ci/README.md b/dev/ci/README.md index 45176581cd..43d680af61 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -75,9 +75,6 @@ We are currently running tests on the following platforms: camlp5, and with warnings as errors; it runs the test-suite and tests the compilation of several external developments. -- Circle CI runs tests that are redundant with GitLab CI and may be removed - eventually. - - Travis CI is used to test the compilation of Coq and run the test-suite on macOS. It also runs a linter that checks whitespace discipline. A [pre-commit hook](../tools/pre-commit) is automatically installed by @@ -165,8 +162,7 @@ automatically built and uploaded to your GitLab registry, and is loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify -the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml), +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) and [`Dockerfile`](docker/bionic_coq/Dockerfile) The Docker building job reuses the uploaded image if it is available, diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a68cd0933e..9259a6e0c8 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -20,10 +20,6 @@ else then export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" export CI_BRANCH="$TRAVIS_BRANCH" - elif [ -n "${CIRCLECI}" ]; - then - export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" - export CI_BRANCH="$CIRCLE_BRANCH" else # assume local CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 6ded97984e..184b90a50b 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" -( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make ) +( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate ) diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh new file mode 100644 index 0000000000..27f588e214 --- /dev/null +++ b/dev/ci/user-overlays/07859-printers.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then + Equations_CI_BRANCH=fix-printers + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations +fi diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index bdaa2aa1a2..e15bcb8e2c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -546,12 +546,12 @@ The printing for one token can be removed with Initially, the pretty-printing table contains the following mapping: -==== === ==== ===== === ==== ==== === -`->` → `<-` ← `*` × -`<=` ≤ `>=` ≥ `=>` ⇒ -`<>` ≠ `<->` ↔ `|-` ⊢ -`\/` ∨ `/\\` ∧ `~` ¬ -==== === ==== ===== === ==== ==== === +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === Any of these can be overwritten or suppressed using the printing commands. diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 323a12357d..f3af318b60 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -48,3 +48,5 @@ val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.ex val type_of_user_symbol : user_symbol -> argument_type val parse_user_entry : string -> string -> user_symbol + +val mlexpr_of_symbol : user_symbol -> MLast.expr diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 0b8d7fda7a..0e2bf55d86 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -128,3 +128,17 @@ let rec parse_user_entry s sep = let s = match s with "hyp" -> "var" | _ -> s in check_separator sep; Uentry s + +let rec mlexpr_of_symbol = function +| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> +| Uentry e -> + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 02da61ef77..07239e7af0 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -15,20 +15,6 @@ open Argextend let plugin_name = <:expr< __coq_plugin_name >> -let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> -| Uentry e -> - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> -| Uentryl (e, l) -> - assert (e = "tactic"); - let wit = <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> - let rec mlexpr_of_clause = function | [] -> <:expr< TyNil >> | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index a2872d07f6..f30c96a7f5 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -14,134 +14,42 @@ open Q_util open Argextend type rule = { - r_head : string option; - (** The first terminal grammar token *) r_patt : extend_token list; (** The remaining tokens of the parsing rule *) r_class : MLast.expr option; (** An optional classifier for the STM *) r_branch : MLast.expr; (** The action performed by this rule. *) - r_depr : unit option; + r_depr : bool; (** Whether this entry is deprecated *) } -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - -let rec make_patt = function - | [] -> <:patt< [] >> - | ExtNonTerminal (_, Some p) :: l -> - <:patt< [ $lid:p$ :: $make_patt l$ ] >> - | _::l -> make_patt l - -let rec make_let e = function - | [] -> e - | ExtNonTerminal (g, Some p) :: l -> - let t = type_of_user_symbol g in - let loc = MLast.loc_of_expr e in - let e = make_let e l in - <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> - | _::l -> make_let e l - -let make_clause { r_patt = pt; r_branch = e; } = - (make_patt pt, - ploc_vala None, - make_let e pt) - -(* To avoid warnings *) -let mk_ignore c pt = - let fold accu = function - | ExtNonTerminal (_, Some p) -> p :: accu - | _ -> accu - in - let names = List.fold_left fold [] pt in - let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in - let names = List.fold_left fold <:expr< () >> names in - <:expr< do { let _ = $names$ in $c$ } >> - -let make_clause_classifier cg s { r_patt = pt; r_class = c; } = - match c ,cg with - | Some c, _ -> - (make_patt pt, - ploc_vala None, - make_let (mk_ignore c pt) pt) - | None, Some cg -> - (make_patt pt, - ploc_vala None, - <:expr< fun loc -> $cg$ $str:s$ >>) - | None, None -> prerr_endline - (("Vernac entry \""^s^"\" misses a classifier. "^ - "A classifier is a function that returns an expression "^ - "of type vernac_classification (see Vernacexpr). You can: ") ^ - "- " ^ ( - ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ - "new vernacular command does not alter the system state;"))^ "\n" ^ - "- " ^ ( - ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ - "new vernacular command alters the system state but not the "^ - "parser nor it starts a proof or ends one;"))^ "\n" ^ - "- " ^ ( - ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ - "a global function f. The function f will be called passing "^ - "\""^s^"\" as the only argument;")) ^ "\n" ^ - "- " ^ ( - "Add a specific classifier in each clause using the syntax:" - ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^ - ("Specific classifiers have precedence over global "^ - "classifiers. Only one classifier is called.") ^ "\n"); - (make_patt pt, - ploc_vala None, - <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) - -let make_fun_clauses loc s l = - let map c = - let depr = match c.r_depr with - | None -> false - | Some () -> true - in - let cl = make_fun loc [make_clause c] in - <:expr< ($mlexpr_of_bool depr$, $cl$)>> - in - mlexpr_of_list map l - -let make_fun_classifiers loc s c l = - let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in - mlexpr_of_list (fun x -> x) cl - -let make_prod_item = function - | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | ExtNonTerminal (g, ido) -> - let nt = type_of_user_symbol g in - let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in - let typ = match ido with None -> None | Some _ -> Some nt in - <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ , - $mlexpr_of_prod_entry_key base g$ ) ) >> - -let mlexpr_of_clause cl = - let mkexpr { r_head = a; r_patt = b; } = match a with - | None -> mlexpr_of_list make_prod_item b - | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) - in - mlexpr_of_list mkexpr cl +let rec make_patt r = function +| [] -> r +| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >> +| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >> +| ExtTerminal _ :: l -> make_patt r l + +let rec mlexpr_of_clause = function +| [] -> <:expr< Vernacentries.TyNil >> +| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> +| ExtNonTerminal (g, id) :: cl -> + let id = mlexpr_of_option mlexpr_of_string id in + <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> + +let make_rule r = + let ty = mlexpr_of_clause r.r_patt in + let cmd = make_patt r.r_branch r.r_patt in + let make_classifier c = make_patt c r.r_patt in + let classif = mlexpr_of_option make_classifier r.r_class in + <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> let declare_command loc s c nt cl = let se = mlexpr_of_string s in - let gl = mlexpr_of_clause cl in - let funcl = make_fun_clauses loc s cl in - let classl = make_fun_classifiers loc s c cl in + let c = mlexpr_of_option (fun x -> x) c in + let rules = mlexpr_of_list make_rule cl in declare_str_items loc - [ <:str_item< do { - CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; - CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; - CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; - } >> ] + [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] open Pcaml @@ -176,38 +84,25 @@ EXTEND ] ] ; deprecation: - [ [ "DEPRECATED" -> () ] ] + [ [ -> false | "DEPRECATED" -> true ] ] ; - (* spiwack: comment-by-guessing: it seems that the isolated string - (which otherwise could have been another argument) is not passed - to the VernacExtend interpreter function to discriminate between - the clauses. *) rule: - [ [ "["; s = STRING; l = LIST0 args; "]"; - d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in - { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } - | "[" ; "-" ; l = LIST1 args ; "]" ; - d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> + [ [ "["; OPT "-"; l = LIST1 args; "]"; + d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in - { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + { r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; + (** The [OPT "-"] argument serves no purpose nowadays, it is left here for + backward compatibility. *) fun_rule: - [ [ "["; s = STRING; l = LIST0 args; "]"; - d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< $e$ >> in - { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } - | "[" ; "-" ; l = LIST1 args ; "]" ; - d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< $e$ >> in - { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + [ [ "["; OPT "-"; l = LIST1 args; "]"; + d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> + { r_patt = l; r_class = c; r_branch = e; r_depr = d; } ] ] ; classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ] + [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ] ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> diff --git a/ide/coq.ml b/ide/coq.ml index 63986935aa..e948360191 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -530,20 +530,31 @@ let break_coqtop coqtop workers = module PrintOpt = struct - type t = string list + type _ t = + | BoolOpt : string list -> bool t + | StringOpt : string list -> string t + + let opt_name (type a) : a t -> string list = function + | BoolOpt l -> l + | StringOpt l -> l + + let opt_data (type a) (key : a t) (v : a) = match key with + | BoolOpt l -> Interface.BoolValue v + | StringOpt l -> Interface.StringValue v (* Boolean options *) - let implicit = ["Printing"; "Implicit"] - let coercions = ["Printing"; "Coercions"] - let raw_matching = ["Printing"; "Matching"] - let notations = ["Printing"; "Notations"] - let all_basic = ["Printing"; "All"] - let existential = ["Printing"; "Existential"; "Instances"] - let universes = ["Printing"; "Universes"] - let unfocused = ["Printing"; "Unfocused"] + let implicit = BoolOpt ["Printing"; "Implicit"] + let coercions = BoolOpt ["Printing"; "Coercions"] + let raw_matching = BoolOpt ["Printing"; "Matching"] + let notations = BoolOpt ["Printing"; "Notations"] + let all_basic = BoolOpt ["Printing"; "All"] + let existential = BoolOpt ["Printing"; "Existential"; "Instances"] + let universes = BoolOpt ["Printing"; "Universes"] + let unfocused = BoolOpt ["Printing"; "Unfocused"] + let diff = StringOpt ["Diffs"] - type bool_descr = { opts : t list; init : bool; label : string } + type 'a descr = { opts : 'a t list; init : 'a; label : string } let bool_items = [ { opts = [implicit]; init = false; label = "Display _implicit arguments" }; @@ -561,24 +572,32 @@ struct { opts = [unfocused]; init = false; label = "Display _unfocused goals" } ] + let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" } + (** The current status of the boolean options *) let current_state = Hashtbl.create 11 - let set opt v = Hashtbl.replace current_state opt v + let set (type a) (opt : a t) (v : a) = + Hashtbl.replace current_state (opt_name opt) (opt_data opt v) let reset () = let init_descr d = List.iter (fun o -> set o d.init) d.opts in - List.iter init_descr bool_items + List.iter init_descr bool_items; + List.iter (fun o -> set o diff_item.init) diff_item.opts let _ = reset () - let printing_unfocused () = Hashtbl.find current_state unfocused + let printing_unfocused () = + let BoolOpt unfocused = unfocused in + match Hashtbl.find current_state unfocused with + | Interface.BoolValue b -> b + | _ -> assert false (** Transmitting options to coqtop *) let enforce h k = - let mkopt o v acc = (o, Interface.BoolValue v) :: acc in + let mkopt o v acc = (o, v) :: acc in let opts = Hashtbl.fold mkopt current_state [] in eval_call (Xmlprotocol.set_options opts) h (function diff --git a/ide/coq.mli b/ide/coq.mli index 40a6dea8d3..3af0aa697e 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -134,13 +134,15 @@ val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query module PrintOpt : sig - type t (** Representation of an option *) + type 'a t (** Representation of an option *) - type bool_descr = { opts : t list; init : bool; label : string } + type 'a descr = { opts : 'a t list; init : 'a; label : string } - val bool_items : bool_descr list + val bool_items : bool descr list - val set : t -> bool -> unit + val diff_item : string descr + + val set : 'a t -> 'a -> unit val printing_unfocused: unit -> bool diff --git a/ide/coqide.ml b/ide/coqide.ml index aa816f2b8b..09a82ba91e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -826,6 +826,7 @@ let refresh_notebook_pos () = let menu = GAction.add_actions let item = GAction.add_action +let radio = GAction.add_radio_action (** Toggle items in menus for printing options *) @@ -1043,7 +1044,19 @@ let build_ui () = ~callback:(fun _ -> show_toolbar#set (not show_toolbar#get)); item "Query Pane" ~label:"_Query Pane" ~accel:"F1" - ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane) + ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane); + GAction.group_radio_actions + ~callback:begin function + | 0 -> List.iter (fun o -> Opt.set o "off") Opt.diff_item.Opt.opts + | 1 -> List.iter (fun o -> Opt.set o "on") Opt.diff_item.Opt.opts + | 2 -> List.iter (fun o -> Opt.set o "removed") Opt.diff_item.Opt.opts + | _ -> assert false + end + [ + radio "Unset diff" 0 ~label:"Unset _Diff"; + radio "Set diff" 1 ~label:"Set Di_ff"; + radio "Set removed diff" 2 ~label:"Set _Removed Diff"; + ]; ]; toggle_items view_menu Coq.PrintOpt.bool_items; @@ -1106,15 +1119,15 @@ let build_ui () = ]; alpha_items templates_menu "Template" Coq_commands.commands; - let qitem s sc ?(dots = true) = - let query = if dots then s ^ "..." else s in + let qitem s sc = + let query = s ^ "..." in item s ~label:("_"^s) ~accel:(modifier_for_queries#get^sc) ~callback:(Query.query query) in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" "K" ~dots:false; + qitem "Search" "K"; qitem "Check" "C"; qitem "Print" "P"; qitem "About" "A"; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 717c4000f5..91c529932f 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -86,6 +86,10 @@ let init () = \n <menuitem action='Display universe levels' />\ \n <menuitem action='Display all low-level contents' />\ \n <menuitem action='Display unfocused goals' />\ +\n <separator/>\ +\n <menuitem action='Unset diff' />\ +\n <menuitem action='Set diff' />\ +\n <menuitem action='Set removed diff' />\ \n </menu>\ \n <menu action='Navigation'>\ \n <menuitem action='Forward' />\ diff --git a/ide/idetop.ml b/ide/idetop.ml index 965bb913ff..854b1abe31 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -530,9 +530,6 @@ let () = Usage.add_to_usage "coqidetop" let islave_init ~opts extra_args = let args = parse extra_args in CoqworkmgrApi.(init High); - let open Coqargs in - if not opts.diffs_set then - Proof_diffs.write_diffs_option "on"; opts, args let () = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c87768b190..715823e5d0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1891,9 +1891,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref in - (* Rem: GApp(_,f,[]) stands for @f *) - DAst.make ?loc @@ - GApp (f, intern_args env args_scopes (List.map fst args)) + (* Rem: GApp(_,f,[]) stands for @f *) + if args = [] then DAst.make ?loc @@ GApp (f,[]) else + smart_gapp f loc (intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> let f,args = match f.CAst.v with diff --git a/interp/declare.ml b/interp/declare.ml index 0222aeb283..532339c03c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -597,27 +597,8 @@ let do_universe poly l = ignore(Lib.add_leaf id (input_universe (src, lev)))) l -type constraint_decl = polymorphic * Univ.Constraint.t - -let cache_constraints (na, (p, c)) = - let ctx = - Univ.ContextSet.add_constraints c - Univ.ContextSet.empty (* No declared universes here, just constraints *) - in cache_universe_context (p,ctx) - -let discharge_constraints (_, (p, c as a)) = - if p then None else Some a - -let input_constraints : constraint_decl -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe constraints") with - cache_function = cache_constraints; - load_function = (fun _ -> cache_constraints); - discharge_function = discharge_constraints; - classify_function = (fun a -> Keep a) } - let do_constraint poly l = + let open Univ in let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in UnivNames.is_polymorphic level, level @@ -639,7 +620,8 @@ let do_constraint poly l = let constraints = List.fold_left (fun acc (l, d, r) -> let p, lu = u_of_id l and p', ru = u_of_id r in check_poly p p'; - Univ.Constraint.add (lu, d, ru) acc) - Univ.Constraint.empty l + Constraint.add (lu, d, ru) acc) + Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (poly, constraints)) + let uctx = ContextSet.add_constraints constraints ContextSet.empty in + declare_universe_context poly uctx diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 4613cd3214..e336ea922d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -501,6 +501,9 @@ let rec compile_lam env cenv lam sz cont = if Array.is_empty args then compile_fv_elem cenv (FVevar evk) sz cont else + (** Arguments are reversed in evar instances *) + let args = Array.copy args in + let () = Array.rev args in comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont diff --git a/kernel/context.ml b/kernel/context.ml index 831dc850fb..4a7204b75c 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -149,6 +149,10 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty + let drop_body = function + | LocalAssum _ as d -> d + | LocalDef (na, v, ty) -> LocalAssum (na, ty) + end (** Rel-context is represented as a list of declarations. @@ -211,6 +215,8 @@ struct | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx in aux [] l + let drop_bodies l = List.Smart.map Declaration.drop_body l + (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) @@ -348,6 +354,10 @@ struct | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + let drop_body = function + | LocalAssum _ as d -> d + | LocalDef (id, v, ty) -> LocalAssum (id, ty) + let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> LocalAssum (f na, t) @@ -403,6 +413,8 @@ struct let to_vars l = List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l + let drop_bodies l = List.Smart.map Declaration.drop_body l + (** [instance_from_named_context Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it diff --git a/kernel/context.mli b/kernel/context.mli index 957ac4b3d6..2b0d36cb8c 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -85,6 +85,9 @@ sig val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't + + (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) + val drop_body : ('c, 't) pt -> ('c, 't) pt end (** Rel-context is represented as a list of declarations. @@ -129,6 +132,9 @@ sig and each {e local definition} is mapped to [false]. *) val to_tags : ('c, 't) pt -> bool list + (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *) + val drop_bodies : ('c, 't) pt -> ('c, 't) pt + (** [extended_list mk n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args] where [mk] is used to build the corresponding variables. @@ -202,6 +208,9 @@ sig val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt + (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) + val drop_body : ('c, 't) pt -> ('c, 't) pt + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. The function provided as the first parameter determines how to translate "names" to "ids". *) val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt @@ -249,6 +258,9 @@ sig (** Return the set of all identifiers bound in a given named-context. *) val to_vars : ('c, 't) pt -> Id.Set.t + (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *) + val drop_bodies : ('c, 't) pt -> ('c, 't) pt + (** [to_instance Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index e97dbd0d67..931b8bbc86 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -135,7 +135,18 @@ and conv_fix env lvl t1 f1 t2 f2 cu = else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in aux 0 cu +let warn_no_native_compiler = + let open Pp in + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + (fun () -> strbrk "Native compiler is disabled," ++ + strbrk " falling back to VM conversion test.") + let native_conv_gen pb sigma env univs t1 t2 = + if not Coq_config.native_compiler then begin + warn_no_native_compiler (); + Vconv.vm_conv_gen pb env univs t1 t2 + end + else let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in match compile ml_filename code ~profile:false with @@ -152,19 +163,8 @@ let native_conv_gen pb sigma env univs t1 t2 = end | _ -> anomaly (Pp.str "Compilation failure.") -let warn_no_native_compiler = - let open Pp in - CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" - (fun () -> strbrk "Native compiler is disabled," ++ - strbrk " falling back to VM conversion test.") - (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = - if not Coq_config.native_compiler then begin - warn_no_native_compiler (); - Vconv.vm_conv cv_pb env t1 t2 - end - else let univs = Environ.universes env in let b = if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2 diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 31ad364911..f784509b6f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -67,6 +67,7 @@ let warn_native_compiler_failed = CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print let call_compiler ?profile:(profile=false) ml_filename = + let () = assert Coq_config.native_compiler in let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in diff --git a/library/goptions.ml b/library/goptions.ml index f14ad333e9..eafcb8fea6 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -318,26 +318,35 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = | Some (name, depr, (read,write,append)) -> write locality (check_and_cast v (read ())) -let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") +let show_value_type = function + | BoolValue _ -> "bool" + | IntValue _ -> "int" + | StringValue _ -> "string" + | StringOptValue _ -> "string" + +let bad_type_error opt_value actual_type = + user_err Pp.(str "Bad type of value for this option:" ++ spc() ++ + str "expected " ++ str (show_value_type opt_value) ++ + str ", got " ++ str actual_type ++ str ".") let check_int_value v = function | IntValue _ -> IntValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "int" let check_bool_value v = function | BoolValue _ -> BoolValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "bool" let check_string_value v = function | StringValue _ -> StringValue v | StringOptValue _ -> StringOptValue (Some v) - | _ -> bad_type_error () + | optv -> bad_type_error optv "string" let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None | StringOptValue _ -> StringOptValue None - | _ -> bad_type_error () + | optv -> bad_type_error optv "nothing" (* Nota: For compatibility reasons, some errors are treated as warning. This allows a script to refer to an option that doesn't diff --git a/library/lib.ml b/library/lib.ml index 8b83261e48..8ebe44890c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -26,13 +26,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of is_type * export * object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_entry = object_name * node +type library_entry = object_name * node -and library_segment = library_entry list +type library_segment = library_entry list type lib_objects = (Names.Id.t * obj) list @@ -73,10 +71,6 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (_,ClosedSection _) :: stk -> clean acc stk - (* LEM; TODO: Understand what this does and see if what I do is the - correct thing for ClosedMod(ule|type) *) - | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" @@ -307,7 +301,6 @@ let end_mod is_type = in let (after,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !lib_state.path_prefix in recalc_path_prefix (); (oname, prefix, fs, after) @@ -555,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -570,7 +562,6 @@ let close_section () = let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); - add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls @@ -589,10 +580,8 @@ let freeze ~marshallable = | n, (CompilingLibrary _ as x) -> Some (n,x) | n, OpenedModule (it,e,op,_) -> Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) - | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection [])) + Some(n,OpenedSection(op,Summary.empty_frozen))) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> diff --git a/library/lib.mli b/library/lib.mli index c6856a55b4..9933b762ba 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,11 +23,9 @@ type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 4e3ba57308..516b04ea21 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -13,23 +13,21 @@ open Formula open Sequent open Rules open Instances -open Constr open Tacmach.New open Tacticals.New +open Globnames let update_flags ()= - let predref=ref Names.Cpred.empty in - let f coe= - try - let kn= fst (destConst (Classops.get_coercion_value coe)) in - predref:=Names.Cpred.add kn !predref - with DestKO -> () + let f acc coe = + match coe.Classops.coe_value with + | ConstRef c -> Names.Cpred.add c acc + | _ -> acc in - List.iter f (Classops.coercions ()); + let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta - (Names.Id.Pred.full,Names.Cpred.complement !predref) + (Names.Id.Pred.full,Names.Cpred.complement pred) let ground_tac solver startseq = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4b834d66d3..636cb8ebf8 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -594,15 +594,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol let clause_of_ty_ml = function | TyML (t,_) -> clause_of_sign t -let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function - | TUentry a -> ExtraArg a - | TUentryl (a,l) -> ExtraArg a - | TUopt(o) -> OptArg (prj o) - | TUlist1 l -> ListArg (prj l) - | TUlist1sep (l,_) -> ListArg (prj l) - | TUlist0 l -> ListArg (prj l) - | TUlist0sep (l,_) -> ListArg (prj l) - let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = fun sign tac -> match sign with @@ -617,7 +608,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i begin fun tac vals ist -> match vals with | [] -> assert false | v :: vals -> - let v' = Taccoerce.Value.cast (topwit (prj a)) v in + let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in f (tac v') vals ist end tac | TyAnonArg (a, sig') -> eval_sign sig' tac diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7ce2dd64af..8ce0316f53 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -24,7 +24,6 @@ open Ltac_plugin open Notation_ops open Notation_term open Glob_term -open Globnames open Stdarg open Genarg open Decl_kinds @@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat = true, cp with _ -> false, [] in let coerce hp coe_index = - let coe = Classops.get_coercion_value coe_index in + let coe_ref = coe_index.Classops.coe_value in try - let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6a63fb02f8..ad33297f0a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -373,6 +373,11 @@ let ltac_interp_realnames lvar = function | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal) | _ as x -> x +let is_patvar pat = + match DAst.get pat with + | PatVar _ -> true + | _ -> false + let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in @@ -381,6 +386,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let typ = nf_evar !evdref j.uj_type in lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = + if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else try try_find_ind env !evdref typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 7ac08e755e..542fb5456c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -42,18 +42,15 @@ type coe_typ = GlobRef.t module CoeTypMap = Refmap_env type coe_info_typ = { - coe_value : constr; - coe_type : types; + coe_value : GlobRef.t; coe_local : bool; - coe_context : Univ.ContextSet.t; coe_is_identity : bool; coe_is_projection : Projection.Repr.t option; - coe_param : int } + coe_param : int; +} let coe_info_typ_equal c1 c2 = - let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in - eq_constr c1.coe_value c2.coe_value && - eq_constr c1.coe_type c2.coe_type && + GlobRef.equal c1.coe_value c2.coe_value && c1.coe_local == c2.coe_local && c1.coe_is_identity == c2.coe_is_identity && c1.coe_is_projection == c2.coe_is_projection && @@ -77,9 +74,7 @@ module IntMap = Map.Make(Int) let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0 -type coe_index = coe_info_typ - -type inheritance_path = coe_index list +type inheritance_path = coe_info_typ list (* table des classes, des coercions et graphe d'heritage *) @@ -300,31 +295,25 @@ let lookup_path_to_fun_from env sigma s = let lookup_path_to_sort_from env sigma s = apply_on_class_of env sigma s lookup_path_to_sort_from_class +let mkNamed = function + | GlobRef.ConstRef c -> EConstr.mkConst c + | VarRef v -> EConstr.mkVar v + | ConstructRef c -> EConstr.mkConstruct c + | IndRef i -> EConstr.mkInd i + let get_coercion_constructor env coe = - let c, _ = - Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value) - in - match EConstr.kind Evd.empty (** FIXME *) c with - | Construct (cstr,u) -> - (cstr, Inductiveops.constructor_nrealargs cstr -1) - | _ -> - raise Not_found + let evd = Evd.from_env env in + let red x = fst (Reductionops.whd_all_stack env evd x) in + match EConstr.kind evd (red (mkNamed coe.coe_value)) with + | Constr.Construct (c, _) -> + c, Inductiveops.constructor_nrealargs c -1 + | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = let i = inductive_class_of s in let j = inductive_class_of t in List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph) -(* coercion_value : coe_index -> unsafe_judgment * bool *) - -let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; - coe_is_identity = b; coe_is_projection = b' } = - let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in - let c' = Vars.subst_univs_level_constr subst c - and t' = Vars.subst_univs_level_constr subst t in - (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx - -(* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = @@ -442,17 +431,13 @@ let cache_coercion env sigma (_, c) = let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in - let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in - let typ = EConstr.Unsafe.to_constr typ in let xf = - { coe_value = value; - coe_type = typ; - coe_context = ctx; + { coe_value = c.coercion_type; coe_local = c.coercion_local; coe_is_identity = c.coercion_is_id; coe_is_projection = c.coercion_is_proj; - coe_param = c.coercion_params } in + coe_param = c.coercion_params; + } in let () = add_new_coercion c.coercion_type xf in add_coercion_in_graph env sigma (xf,is,it) @@ -531,8 +516,6 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps Lib.add_anonymous_leaf (inCoercion c) (* For printing purpose *) -let get_coercion_value v = v.coe_value - let pr_cl_index = Bijint.Index.print let classes () = Bijint.dom !class_tab diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 8df085e15c..af00c0a8dc 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -39,16 +39,19 @@ type cl_info_typ = { type coe_typ = GlobRef.t (** This is the type of infos for declared coercions *) -type coe_info_typ +type coe_info_typ = { + coe_value : GlobRef.t; + coe_local : bool; + coe_is_identity : bool; + coe_is_projection : Projection.Repr.t option; + coe_param : int; +} (** [cl_index] is the type of class keys *) type cl_index -(** [coe_index] is the type of coercion keys *) -type coe_index - (** This is the type of paths from a class to another *) -type inheritance_path = coe_index list +type inheritance_path = coe_info_typ list (** {6 Access to classes infos } *) @@ -79,8 +82,6 @@ val declare_coercion : (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool -val coercion_value : coe_index -> (unsafe_judgment * bool * Projection.Repr.t option) Univ.in_universe_context_set - (** {6 Lookup functions for coercion paths } *) (** @raise Not_found in the following functions when no path exists *) @@ -105,10 +106,9 @@ val install_path_printer : val string_of_class : cl_typ -> string val pr_class : cl_typ -> Pp.t val pr_cl_index : cl_index -> Pp.t -val get_coercion_value : coe_index -> Constr.t val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list val classes : unit -> cl_typ list -val coercions : unit -> coe_index list +val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c6c2f57dd4..5e3821edf1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -369,8 +369,11 @@ let apply_coercion env sigma p hj typ_cl = let j,t,evd = List.fold_left (fun (ja,typ_cl,sigma) i -> - let ((fv,isid,isproj),ctx) = coercion_value i in - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + let isid = i.coe_is_identity in + let isproj = i.coe_is_projection in + let sigma, c = new_global sigma i.coe_value in + let typ = Retyping.get_type_of env sigma c in + let fv = make_judge c typ in let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let sigma, jres = apply_coercion_args env sigma true isproj argl fv diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c944080503..255707dc7b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -209,6 +209,9 @@ and nf_evar env sigma evk stk = | Zapp args :: stk -> (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that really an invariant? *) + (** Let-bound arguments are present in the evar arguments but not in the + type, so we turn the let into a product. *) + let hyps = Context.Named.drop_bodies hyps in let fold accu d = Term.mkNamedProd_or_LetIn d accu in let t = List.fold_left fold concl hyps in let t, args = nf_args env sigma args t in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd7135b6a6..1810cc6588 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -98,7 +98,8 @@ let print_ref reduce ref udecl = (Array.to_list (Univ.Instance.to_array inst)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = - if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ @@ -552,8 +553,7 @@ let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in - pr_universe_instance sigma univs + pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = @@ -657,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function @@ -793,9 +789,6 @@ let read_sec_context qid = let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection _)::rest -> - user_err Pp.(str "Cannot print the contents of a closed section.") - (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -909,7 +902,7 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) +let print_coercion_value env sigma v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in diff --git a/printing/printer.ml b/printing/printer.ml index ba094596ff..a77c1ced56 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -290,11 +290,13 @@ let pr_cumulativity_info sigma cumi = let pr_global_env = pr_global_env let pr_global = pr_global_env Id.Set.empty -let pr_puniverses f env (c,u) = - f env c ++ - (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - else mt ()) +let pr_universe_instance evd inst = + str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + +let pr_puniverses f env sigma (c,u) = + if !Constrextern.print_universes + then f env c ++ pr_universe_instance sigma u + else f env c let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) let pr_existential_key = Termops.pr_existential_key @@ -1016,10 +1018,6 @@ let pr_polymorphic b = if b then str"Polymorphic " else str"Monomorphic " else mt () -let pr_universe_instance evd ctx = - let inst = Univ.UContext.instance ctx in - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" - (* print the proof step, possibly with diffs highlighted, *) let print_and_diff oldp newp = match newp with diff --git a/printing/printer.mli b/printing/printer.mli index 948b06f3f6..971241d5f9 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -120,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t @@ -139,9 +139,9 @@ val pr_constructor : env -> constructor -> Pp.t val pr_inductive : env -> inductive -> Pp.t val pr_evaluable_reference : evaluable_global_reference -> Pp.t -val pr_pconstant : env -> pconstant -> Pp.t -val pr_pinductive : env -> pinductive -> Pp.t -val pr_pconstructor : env -> pconstructor -> Pp.t +val pr_pconstant : env -> evar_map -> pconstant -> Pp.t +val pr_pinductive : env -> evar_map -> pinductive -> Pp.t +val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t (** Contexts *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 3f95dcfb6d..e2d9850bf8 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then - let ctx = Declareops.inductive_polymorphic_context mib in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - Printer.pr_universe_instance sigma ctx + Printer.pr_universe_instance sigma u else mt () in hov 0 ( diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 6be80d29a5..eca0c6674b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -42,13 +42,6 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w -let classifiers = ref [] -let declare_vernac_classifier - (s : Vernacexpr.extend_name) - (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) -= - classifiers := !classifiers @ [s,f] - let idents_of_name : Names.Name.t -> Names.Id.t list = function | Names.Anonymous -> [] @@ -194,7 +187,7 @@ let classify_vernac e = | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try List.assoc s !classifiers l () + try Vernacentries.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 45fbfb42af..e82b191418 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -9,17 +9,12 @@ (************************************************************************) open Vernacexpr -open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) val classify_vernac : vernac_control -> vernac_classification -(** Install a vernacular classifier for VernacExtend *) -val declare_vernac_classifier : - Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit - (** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification diff --git a/tactics/hints.ml b/tactics/hints.ml index 09b2e59cea..43a450ea71 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -886,20 +886,6 @@ let pr_hint_term env sigma ctx = function let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in pr_econstr_env env sigma c -(** We need an object to record the side-effect of registering - global universes associated with a hint. *) -let cache_context_set (_,c) = - Global.push_context_set false c - -let input_context_set : Univ.ContextSet.t -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe context") with - cache_function = cache_context_set; - load_function = (fun _ -> cache_context_set); - discharge_function = (fun (_,a) -> Some a); - classify_function = (fun a -> Keep a) } - let warn_polymorphic_hint = CWarnings.create ~name:"polymorphic-hint" ~category:"automation" (fun hint -> strbrk"Using polymorphic hint " ++ hint ++ @@ -919,7 +905,7 @@ let fresh_global_or_constr env sigma poly cr = else begin if isgr then warn_polymorphic_hint (pr_hint_term env sigma ctx cr); - Lib.add_anonymous_leaf (input_context_set ctx); + Declare.declare_universe_context false ctx; (c, Univ.ContextSet.empty) end @@ -1315,7 +1301,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) - else (Lib.add_anonymous_leaf (input_context_set diff); + else (Declare.declare_universe_context false diff; IsConstr (c', Univ.ContextSet.empty)) let project_hint ~poly pri l2r r = diff --git a/test-suite/Makefile b/test-suite/Makefile index 33b4023272..b8aac8b6f8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -192,10 +192,6 @@ PRINT_LOGS?= TRAVIS?= # special because we want to print travis_fold directives ifdef APPVEYOR PRINT_LOGS:=APPVEYOR -else -ifdef CIRCLECI -PRINT_LOGS:=CIRCLECI -endif #CIRCLECI endif #APPVEYOR report: summary.log diff --git a/test-suite/bugs/closed/2733.v b/test-suite/bugs/closed/2733.v index 832de4f913..24dd30b32e 100644 --- a/test-suite/bugs/closed/2733.v +++ b/test-suite/bugs/closed/2733.v @@ -16,6 +16,21 @@ match k,l with |B,l' => Bcons true (Ncons 0 l') end. +(* At some time, the success of trullynul was dependent on the name of + the variables! *) + +Definition trullynul2 k {a} (l : alt_list k a) := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + +Definition trullynul3 k {z} (l : alt_list k z) := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 -> alt_list t1 t3 := match l with diff --git a/test-suite/bugs/closed/8119.v b/test-suite/bugs/closed/8119.v new file mode 100644 index 0000000000..c6329a7328 --- /dev/null +++ b/test-suite/bugs/closed/8119.v @@ -0,0 +1,46 @@ +Require Import Coq.Strings.String. + +Section T. + Eval vm_compute in let x := tt in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval vm_compute in let _ := Set in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval vm_compute in let _ := Prop in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End T. + +Section U0. + Let n : unit := tt. + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End U0. + +Section S0. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End S0. + +Class T := { }. +Section S1. + Context {p : T}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) +End S1. + +Class M := { m : Type }. +Section S2. + Context {p : M}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) +End S2. diff --git a/test-suite/bugs/closed/8126.v b/test-suite/bugs/closed/8126.v new file mode 100644 index 0000000000..f52dfc6b47 --- /dev/null +++ b/test-suite/bugs/closed/8126.v @@ -0,0 +1,13 @@ +(* See also output test Notations4.v *) + +Inductive foo := tt. +Bind Scope foo_scope with foo. +Delimit Scope foo_scope with foo. +Notation "'HI'" := tt : foo_scope. +Definition myfoo (x : nat) (y : nat) (z : foo) := y. +Notation myfoo0 := (@myfoo 0). +Notation myfoo01 := (@myfoo0 1). +Check myfoo 0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 tt. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 HI. (* was failing *) diff --git a/test-suite/output/BadOptionValueType.out b/test-suite/output/BadOptionValueType.out new file mode 100644 index 0000000000..34d8518a75 --- /dev/null +++ b/test-suite/output/BadOptionValueType.out @@ -0,0 +1,8 @@ +The command has indeed failed with message: +Bad type of value for this option: expected int, got string. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got string. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got int. +The command has indeed failed with message: +Bad type of value for this option: expected bool, got int. diff --git a/test-suite/output/BadOptionValueType.v b/test-suite/output/BadOptionValueType.v new file mode 100644 index 0000000000..b61c3757ba --- /dev/null +++ b/test-suite/output/BadOptionValueType.v @@ -0,0 +1,4 @@ +Fail Set Default Timeout "2". +Fail Set Debug Eauto "yes". +Fail Set Debug Eauto 1. +Fail Set Implicit Arguments 1. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 419dcadb4c..dfab400baa 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -169,3 +169,5 @@ fun x : K => match x with | _ => 2 end : K -> nat +The command has indeed failed with message: +Pattern "S _, _" is redundant in this clause. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4740c009a4..e4fa7044e7 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -217,3 +217,6 @@ Check fun x => match x with a3 | a4 => 3 | _ => 2 end. Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end. Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end. Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end. + +(* Test redundant clause within a disjunctive pattern *) +Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 5ab616160a..d32cf67e28 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -246,3 +246,9 @@ Notation ============================ ##@% ^^^ +myfoo01 tt + : nat +myfoo01 tt + : nat +myfoo01 tt + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 876aaa3944..180e8d337e 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -399,3 +399,14 @@ Show. Abort. End Issue7731. + +Module Issue8126. + +Definition myfoo (x : nat) (y : nat) (z : unit) := y. +Notation myfoo0 := (@myfoo 0). +Notation myfoo01 := (@myfoo0 1). +Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) + +End Issue8126. diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 048d4d93a0..c5dedc880e 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -64,6 +64,15 @@ let make_rule f prod = let act = ty_eval ty_rule f in Extend.Rule (symb, act) +let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function +| TUentry a -> ExtraArg a +| TUentryl (a,l) -> ExtraArg a +| TUopt(o) -> OptArg (proj_symbol o) +| TUlist1 l -> ListArg (proj_symbol l) +| TUlist1sep (l,_) -> ListArg (proj_symbol l) +| TUlist0 l -> ListArg (proj_symbol l) +| TUlist0sep (l,_) -> ListArg (proj_symbol l) + (** Vernac grammar extensions *) let vernac_exts = ref [] diff --git a/vernac/egramml.mli b/vernac/egramml.mli index a5ee036db5..c4f4fcfaa4 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -26,6 +26,8 @@ val extend_vernac_command_grammar : val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list +val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type + (** Utility function reused in Egramcoq : *) val make_rule : diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c49ffe2679..b9c47ff475 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -194,12 +194,6 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let pr_puniverses f env (c,u) = - f env c ++ - (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - else mt()) - let explain_elim_arity env sigma ind sorts c pj okinds = let open EConstr in let env = make_all_name_different env sigma in @@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty = let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ spc () ++ strbrk "the branch for constructor" ++ spc () ++ - quote (pr_puniverses pr_constructor env ci) ++ + quote (pr_pconstructor env sigma ci) ++ spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." @@ -1233,12 +1227,7 @@ let explain_wrong_numarg_inductive env ind n = str " expects " ++ decline_string n "argument" ++ str "." let explain_unused_clause env pats = -(* Without localisation - let s = if List.length pats > 1 then "s" else "" in - (str ("Unused clause with pattern"^s) ++ spc () ++ - hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")") -*) - str "This clause is redundant." + str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause." let explain_non_exhaustive env pats = str "Non exhaustive pattern-matching: no clause found for " ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b6bc76a2ed..653f8b26e0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2436,3 +2436,121 @@ let interp ?verbosely ?proof ~st cmd = let exn = CErrors.push exn in Vernacstate.invalidate_cache (); iraise exn + +(** VERNAC EXTEND registering *) + +open Genarg +open Extend + +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") + +let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args +| TyNonTerminal (_, tu, ty) -> fun f args -> + begin match args with + | [] -> type_error () + | Genarg.GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_classifier ty (f v) args + end + +(** Stupid GADTs forces us to duplicate the definition just for typing *) +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_command ty f args +| TyNonTerminal (_, tu, ty) -> fun f args -> + begin match args with + | [] -> type_error () + | Genarg.GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_command ty (f v) args + end + +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function +| TUlist1 l -> Alist1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUlist0 l -> Alist0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUopt o -> Aopt (untype_user_symbol o) +| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a)) +| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i) + +let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function +| TyNil -> [] +| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty +| TyNonTerminal (id, tu, ty) -> + let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in + let symb = untype_user_symbol tu in + Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty + +let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol + +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let vernac_extend ~command ?classifier ?entry ext = + let get_classifier (TyML (_, ty, _, cl)) = match cl with + | Some cl -> untype_classifier ty cl + | None -> + match classifier with + | Some cl -> fun _ -> cl command + | None -> + let e = match entry with + | None -> "COMMAND" + | Some e -> Pcoq.Gram.Entry.name e + in + let msg = Printf.sprintf "\ + Vernac entry \"%s\" misses a classifier. \ + A classifier is a function that returns an expression \ + of type vernac_classification (see Vernacexpr). You can: \n\ + - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ + new vernacular command does not alter the system state;\n\ + - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ + new vernacular command alters the system state but not the \ + parser nor it starts a proof or ends one;\n\ + - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ + a global function f. The function f will be called passing\ + \"%s\" as the only argument;\n\ + - Add a specific classifier in each clause using the syntax:\n\ + '[...] => [ f ] -> [...]'.\n\ + Specific classifiers have precedence over global \ + classifiers. Only one classifier is called." + command e e e command + in + CErrors.user_err (Pp.strbrk msg) + in + let cl = Array.map_of_list get_classifier ext in + let iter i (TyML (depr, ty, f, _)) = + let f = untype_command ty f in + let r = untype_grammar ty in + let () = vinterp_add depr (command, i) f in + Egramml.extend_vernac_command_grammar (command, i) entry r + in + let () = declare_vernac_classifier command cl in + List.iteri iter ext diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 79f9c05ad8..fb2a30bac7 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -42,3 +42,33 @@ val universe_polymorphism_option_name : string list (** Elaborate a [atts] record out of a list of flags. Also returns whether polymorphism is explicitly (un)set. *) val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts + +(** {5 VERNAC EXTEND} *) + +type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + string option * + ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> + ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +(** Wrapper to dynamically extend vernacular commands. *) +val vernac_extend : + command:string -> + ?classifier:(string -> Vernacexpr.vernac_classification) -> + ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> + ty_ml list -> unit + +(** {5 STM classifiers} *) + +val get_vernac_classifier : + Vernacexpr.extend_name -> classifier + +(** Low-level API, not for casual user. *) +val declare_vernac_classifier : + string -> classifier array -> unit |