diff options
67 files changed, 558 insertions, 401 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b39e74ffee..8fd5eb3972 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -640,9 +640,6 @@ library:ci-fiat-crypto: - library:ci-coqprime - plugin:ci-rewriter -library:ci-fiat-crypto-legacy: - extends: .ci-template-flambda - library:ci-flocq: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index 10c3b027c3..f14203fa4a 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -25,7 +25,6 @@ CI_TARGETS= \ ci-equations \ ci-fcsl-pcm \ ci-fiat-crypto \ - ci-fiat-crypto-legacy \ ci-fiat_parsers \ ci-flocq \ ci-geocoq \ diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 051f51bbb3..62e732ce69 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -170,7 +170,6 @@ let check_inductive env mind mb = check_guarded = mb_flags.check_guarded; check_positive = mb_flags.check_positive; check_universes = mb_flags.check_universes; - check_template = mb_flags.check_template; conv_oracle = mb_flags.conv_oracle; } env diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d115744707..8854a23dd5 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -56,10 +56,6 @@ let pr_nonpositive env = let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in pr_assumptions "Inductives whose positivity is assumed" inds -let pr_unsafe_template env = - let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_template then MutInd.to_string c :: acc else acc) env [] in - pr_assumptions "Inductives using unchecked template polymorphism" inds - let print_context env = if !output_context then begin Feedback.msg_notice @@ -70,8 +66,8 @@ let print_context env = str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_unsafe_template env))) + str "* " ++ hov 0 (pr_nonpositive env ++ fnl())) + ) end let stats env = diff --git a/checker/values.ml b/checker/values.ml index c8bbc092b4..ed730cff8e 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -238,7 +238,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 608cc127a0..60c266699c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -165,13 +165,6 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# fiat_crypto_legacy -######################################################################## -: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" -: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" -: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" - -######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh deleted file mode 100755 index 9ce5da9f50..0000000000 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -FORCE_GIT=1 -git_download fiat_crypto_legacy - -fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" -fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display" - -( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ - ./etc/ci/remove_autogenerated.sh && \ - make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index f08a08531f..c8ea59f08a 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -91,7 +91,6 @@ let projects = { cross_crypto = callPackage ./cross_crypto.nix {}; Elpi = callPackage ./Elpi.nix {}; fiat_crypto = callPackage ./fiat_crypto.nix {}; - fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; flocq = callPackage ./flocq.nix {}; formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix deleted file mode 100644 index 3248665579..0000000000 --- a/dev/ci/nix/fiat_crypto_legacy.nix +++ /dev/null @@ -1,6 +0,0 @@ -{}: - -{ - configure = "./etc/ci/remove_autogenerated.sh"; - make = "make print-old-pipeline-lite old-pipeline-lite lite-display"; -} diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh new file mode 100644 index 0000000000..fd63980036 --- /dev/null +++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then + + quickchick_CI_REF=non_maximal_implicit + quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick + + elpi_CI_REF=non_maximal_implicit + elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 3bc92e6aee..cb6e695865 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -17,6 +17,11 @@ Printers: Constrextern.extern_constr which were taking a boolean argument for the goal style now take instead a label. +Implicit arguments: + +- The type `Impargs.implicit_kind` was removed in favor of + `Glob_term.binding_kind`. + ## Changes between Coq 8.10 and Coq 8.11 ### ML API diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst new file mode 100644 index 0000000000..57bce7e4f6 --- /dev/null +++ b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst @@ -0,0 +1,7 @@ +- **Changed:** + Warn when manual implicit arguments are used in unexpected positions + of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit + argument name is shadowed (e.g. in `Check fun f : forall {x:nat} + {x}, nat => f`) + (`#10202 <https://github.com/coq/coq/pull/10202>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst new file mode 100644 index 0000000000..d8ff1fec31 --- /dev/null +++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax for non maximal implicit arguments in definitions and terms using + square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` + to be consistent with the command :cmd:`Arguments (implicits)`. + (`#11235 <https://github.com/coq/coq/pull/11235>`_, + by SimonBoulier). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 510e271951..7b4b652a6a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1570,11 +1570,26 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag. +Each implicit argument can be declared to be inserted maximally or non +maximally. In Coq, maximally-inserted implicit arguments are written between curly braces +"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". -.. seealso:: :ref:`displaying-implicit-args`. +.. seealso:: :flag:`Maximal Implicit Insertion` + +Trailing Implicit Arguments ++++++++++++++++++++++++++++ + +An implicit argument is considered trailing when all following arguments are declared +implicit. Trailing implicit arguments cannot be declared non maximally inserted, +otherwise they would never be inserted. + +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. + + For instance: + + .. coqtop:: all fail + + Fail Definition double [n] := n + n. Casual use of implicit arguments @@ -1608,7 +1623,7 @@ Implicit Argument Binders In the first setting, one wants to explicitly give the implicit arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly -braces: +braces or square braces: .. coqtop:: all @@ -1624,6 +1639,17 @@ absent in every situation but still be able to specify it if needed: Goal forall A, compose id id = id (A:=A). +For non maximally inserted implicit arguments, use square brackets: + +.. coqtop:: all + + Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map f t) + end. + + Print Implicit map. The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype @@ -1643,6 +1669,44 @@ For example: One can always specify the parameter if it is not uniform using the usual implicit arguments disambiguation syntax. +The syntax is also supported in internal binders. For instance, in the +following kinds of expressions, the type of each declaration present +in :token:`binders` can be bracketed to mark the declaration as +implicit: +:n:`fun (@ident:forall @binders, @type) => @term`, +:n:`forall (@ident:forall @binders, @type), @type`, +:n:`let @ident @binders := @term in @term`, +:n:`fix @ident @binders := @term in @term` and +:n:`cofix @ident @binders := @term in @term`. +Here is an example: + +.. coqtop:: all + + Axiom Ax : + forall (f:forall {A} (a:A), A * A), + let g {A} (x y:A) := (x,y) in + f 0 = g 0 0. + +.. warn:: Ignoring implicit binder declaration in unexpected position + + This is triggered when setting an argument implicit in an + expression which does not correspond to the type of an assumption + or to the body of a definition. Here is an example: + + .. coqtop:: all warn + + Definition f := forall {y}, y = 0. + +.. warn:: Making shadowed name of implicit argument accessible by position + + This is triggered when two variables of same name are set implicit + in the same block of binders, in which case the first occurrence is + considered to be unnamed. Here is an example: + + .. coqtop:: all warn + + Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. + Declaring Implicit Arguments ++++++++++++++++++++++++++++ @@ -1728,14 +1792,6 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. - - For instance in - - .. coqtop:: all fail - - Arguments prod _ [_]. - Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1811,7 +1867,7 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Implicit Arguments @@ -1823,7 +1879,7 @@ Mode for automatic declaration of implicit arguments .. _controlling-strict-implicit-args: Controlling strict implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++ .. flag:: Strict Implicit @@ -1842,7 +1898,7 @@ Controlling strict implicit arguments .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++ .. flag:: Contextual Implicit @@ -1853,7 +1909,7 @@ Controlling contextual implicit arguments .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Reversible Pattern Implicit @@ -1864,7 +1920,7 @@ Controlling reversible-pattern implicit arguments .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Maximal Implicit Insertion @@ -1873,6 +1929,28 @@ Controlling the insertion of implicit arguments not followed by explicit argumen function is partially applied and the next argument of the function is an implicit one. +Combining manual declaration and automatic declaration +++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +When some arguments are manually specified implicit with binders in a definition +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. + +In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, +some trailing implicit arguments can be inferred to be non maximally inserted. In +this case, they are converted to maximally inserted ones. + +.. example:: + + .. coqtop:: all + + Set Implicit Arguments. + Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. + Print Implicit eq0_le0. + Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. + Print Implicit eq0_le0'. + + .. _explicit-applications: Explicit applications @@ -2136,8 +2214,10 @@ Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ .. index:: `{ } +.. index:: `[ ] .. index:: `( ) .. index:: `{! } +.. index:: `[! ] .. index:: `(! ) Implicit generalization is an automatic elaboration of a statement @@ -2145,11 +2225,12 @@ with free variables into a closed statement where these variables are quantified explicitly. It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ } or \`( ). +surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, and terms surrounded by \`( ) introduce -them as explicit arguments. +inserted implicit arguments, terms surrounded by \`[ ] introduce them as +non maximally inserted implicit arguments and terms surrounded by \`( ) +introduce them as explicit arguments. Generalizing binders always introduce their free variables as maximally inserted implicit arguments. The binder itself introduces diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index d591718b17..09090ce89a 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -283,8 +283,10 @@ Binders | ( {+ @name } : @term ) | ( @name {? : @term } := @term ) | %{ {+ @name } {? : @term } %} + | [ {+ @name } {? : @term } ] | `( {+, @typeclass_constraint } ) | `%{ {+, @typeclass_constraint } %} + | `[ {+, @typeclass_constraint } ] | ' @pattern0 | ( @name : @term %| @term ) typeclass_constraint ::= {? ! } @term diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index ff0b90dcff..e1b9c6b7cb 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -831,8 +831,9 @@ let rec print_symbol : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit = fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t (if osep then " OPT_SEP" else "") | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s - | Stoken p when L.tok_pattern_strings p <> ("", None) -> + | Stoken p -> begin match L.tok_pattern_strings p with + | "", Some s -> print_str ppf s | con, Some prm -> fprintf ppf "%s@ %a" con print_str prm | con, None -> fprintf ppf "%s" con end | Snterml (e, l) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f4ae5bf676..2ceea58297 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -257,7 +257,7 @@ type intern_env = { tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; - impl_binder_index: int option; + binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option; } (**********************************************************************) @@ -330,15 +330,18 @@ let exists_name na l = | _ -> false let build_impls ?loc n bk na acc = - match bk with - | Implicit -> + let impl_status max = let na = - if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end - else na in + if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end + else na in let impl = match na with - | Name id -> Some (ExplByName id,Manual,(true,true)) - | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in - impl :: acc + | Name id -> Some (ExplByName id,Manual,(max,true)) + | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in + impl + in + match bk with + | NonMaxImplicit -> impl_status false :: acc + | MaxImplicit -> impl_status true :: acc | Explicit -> None :: acc let impls_binder_list = @@ -373,6 +376,49 @@ let rec check_capture ty = let open CAst in function | [] -> () +(** Status of the internalizer wrt "Arguments" of names *) + +let restart_no_binders env = + { env with binder_block_names = None} + (* Not in relation with the "Arguments" of a name *) + +let restart_prod_binders env = + { env with binder_block_names = Some (Some AbsPi, Id.Set.empty) } + (* In a position binding a type to a name *) + +let restart_lambda_binders env = + { env with binder_block_names = Some (Some AbsLambda, Id.Set.empty) } + (* In a position binding a body to a name *) + +let switch_prod_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsLambda -> restart_prod_binders env + | _ -> restart_no_binders env + (* In a position switching to a type *) + +let switch_lambda_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsPi -> restart_lambda_binders env + | _ -> restart_no_binders env + (* In a position switching to a term *) + +let slide_binders env = + match env.binder_block_names with + | Some (o,ids) when o <> Some AbsPi -> restart_prod_binders env + | _ -> restart_no_binders env + (* In a position of cast *) + +let binder_status_fun = { + no = (fun x -> x); + restart_prod = on_snd restart_prod_binders; + restart_lambda = on_snd restart_lambda_binders; + switch_prod = on_snd switch_prod_binders; + switch_lambda = on_snd switch_lambda_binders; + slide = on_snd slide_binders; +} + +(**) + let locate_if_hole ?loc na c = match DAst.get c with | GHole (_,naming,arg) -> (try match na with @@ -397,7 +443,11 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "the type of a constructor shall use a different name.") let pure_push_name_env (id,implargs) env = - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + {env with + ids = Id.Set.add id env.ids; + impls = Id.Map.add id implargs env.impls; + binder_block_names = Option.map (fun (b,ids) -> (b,Id.Set.add id ids)) env.binder_block_names; + } let push_name_env ntnvars implargs env = let open CAst in @@ -421,13 +471,15 @@ let remember_binders_impargs env bl = let restore_binders_impargs env l = List.fold_right pure_push_name_env l env -let warn_unexpected_implicit_binder_declaration = +let warn_ignoring_unexpected_implicit_binder_declaration = CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax" - Pp.(fun () -> str "Unexpected implicit binder declaration.") + Pp.(fun () -> str "Ignoring implicit binder declaration in unexpected position.") let check_implicit_meaningful ?loc k env = - if k = Implicit && env.impl_binder_index = None then - warn_unexpected_implicit_binder_declaration ?loc () + if k <> Explicit && env.binder_block_names = None then + (warn_ignoring_unexpected_implicit_binder_declaration ?loc (); Explicit) + else + k let intern_generalized_binder intern_type ntnvars env {loc;v=na} b' t ty = @@ -441,10 +493,10 @@ let intern_generalized_binder intern_type ntnvars let env' = List.fold_left (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) env fvs in - check_implicit_meaningful ?loc b' env; + let b' = check_implicit_meaningful ?loc b' env in let bl = List.map CAst.(map (fun id -> - (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) + (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -463,7 +515,7 @@ let intern_generalized_binder intern_type ntnvars (make ?loc (na,b',ty')) :: List.rev bl) let intern_assumption intern ntnvars env nal bk ty = - let intern_type env = intern (set_type_scope env) in + let intern_type env = intern (restart_prod_binders (set_type_scope env)) in match bk with | Default k -> let ty = intern_type env ty in @@ -471,7 +523,7 @@ let intern_assumption intern ntnvars env nal bk ty = let impls = impls_type_list 1 ty in List.fold_left (fun (env, bl) ({loc;v=na} as locna) -> - check_implicit_meaningful ?loc k env; + let k = check_implicit_meaningful ?loc k env in (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal @@ -492,8 +544,8 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = - let term = intern env def in - let ty = Option.map (intern env) ty in + let term = intern (reset_tmp_scope (restart_lambda_binders env)) def in + let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in (push_name_env ntnvars impls env locna, (na,Explicit,term,ty)) @@ -713,6 +765,19 @@ let flatten_binders bl = | a -> [a] in List.flatten (List.map dispatch bl) +let rec adjust_env env = function + (* We need to adjust scopes, binder blocks ... to the env expected + at the recursive occurrence; We do an underapproximation... *) + | NProd (_,_,c) -> adjust_env (switch_prod_binders env) c + | NLambda (_,_,c) -> adjust_env (switch_lambda_binders env) c + | NLetIn (_,_,_,c) -> adjust_env env c + | NVar id when Id.equal id ldots_var -> env + | NCast (c,_) -> adjust_env env c + | NApp _ -> restart_no_binders env + | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NInt _ | NFloat _ + | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *) + let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let (terms,termlists,binders,binderlists) = subst in (* when called while defining a notation, avoid capturing the private binders @@ -725,7 +790,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let rec aux_letin env = function | [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator | AddPreBinderIter (y,binder)::rest,terminator,iter -> - let env,binders = intern_local_binder_aux intern ntnvars (env,[]) binder in + let env,binders = intern_local_binder_aux intern ntnvars (adjust_env env iter,[]) binder in let binder,extra = flatten_generalized_binders_if_any y binders in aux (terms,Some (y,binder),Some (extra@rest,terminator,iter)) (renaming,env) iter | AddBinderIter (y,binder)::rest,terminator,iter -> @@ -733,7 +798,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | AddTermIter nterms::rest,terminator,iter -> aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter | AddLetIn (na,c,t)::rest,terminator,iter -> - let env,(na,_,c,t) = intern_letin_binder intern ntnvars env (na,c,t) in + let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id @@ -823,7 +888,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc - (traverse_binder intern_pat ntnvars subst avoid) (aux subst') subinfos t + (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -1144,7 +1209,7 @@ let interp_reference vars r = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env; - impl_binder_index = None} + binder_block_names = None} Environ.empty_named_context_val (vars, Id.Map.empty) None [] r in r @@ -1892,6 +1957,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (false,iddef))) in + let env = restart_lambda_binders env in let idl_temp = Array.map (fun (id,recarg,bl,ty,_) -> let recarg = Option.map (function { CAst.v = v } -> match v with @@ -1934,6 +2000,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (true,iddef))) in + let env = restart_lambda_binders env in let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in @@ -1957,18 +2024,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (_,_,bd) -> bd) idl) | CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.") | CProdN (bl,c2) -> - let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in + let (env',bl) = List.fold_left intern_local_binder (switch_prod_binders env,[]) bl in expand_binders ?loc mkGProd bl (intern_type env' c2) | CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.") | CLambdaN (bl,c2) -> - let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in + let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope (switch_lambda_binders env),[]) bl in expand_binders ?loc mkGLambda bl (intern env' c2) | CLetIn (na,c1,t,c2) -> - let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in - let int = Option.map (intern_type_restart_implicit env) t in + let inc1 = intern_restart_binders (reset_tmp_scope env) c1 in + let int = Option.map (intern_type_restart_binders env) t in DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, - intern_restart_implicit (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) + intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) @@ -2009,7 +2076,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args - | _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in + | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in apply_impargs c env impargs args_scopes (merge_impargs l args) loc @@ -2053,7 +2120,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) - (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in + (Id.Set.union ex_ids as_in_vars) + (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = let rec aux = function @@ -2063,7 +2131,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in aux match_from_in in let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with - | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) + | [] -> Option.map (intern_type (slide_binders env')) rtnpo (* Only PatVar in "in" clauses *) | l -> (* Build a return predicate by expansion of the patterns of the "in" clause *) let thevars, thepats = List.split l in @@ -2071,7 +2139,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') + Option.cata (intern_type_no_implicit env') (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = @@ -2090,7 +2158,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let p' = Option.map (fun u -> let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (CAst.make na') in - intern_type env'' u) po in + intern_type (slide_binders env'') u) po in DAst.make ?loc @@ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) @@ -2100,7 +2168,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let p' = Option.map (fun p -> let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (CAst.make na') in - intern_type env'' p) po in + intern_type (slide_binders env'') p) po in DAst.make ?loc @@ GIf (c', (na', p'), intern env b1, intern env b2) | CHole (k, naming, solve) -> @@ -2160,18 +2228,20 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, map_cast_type (intern_type env) c2) + GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) ) and intern_type env = intern (set_type_scope env) - and intern_no_implicit env = intern {env with impl_binder_index = None} + and intern_type_no_implicit env = intern (restart_no_binders (set_type_scope env)) - and intern_restart_implicit env = intern {env with impl_binder_index = Some 0} + and intern_no_implicit env = intern (restart_no_binders env) - and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0} + and intern_restart_binders env = intern (restart_lambda_binders env) + + and intern_type_restart_binders env = intern (restart_prod_binders (set_type_scope env)) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = - intern_local_binder_aux intern_restart_implicit ntnvars env bind + intern_local_binder_aux intern ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n pl = @@ -2198,7 +2268,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in - let rhs' = intern {env with ids = env_ids} rhs in + let rhs' = intern_no_implicit {env with ids = env_ids} rhs in CAst.make ?loc (eqn_ids,pl,rhs')) pll and intern_case_item env forbidden_names_for_gen (tm,na,t) = @@ -2336,7 +2406,12 @@ let extract_ids env = let scope_of_type_kind sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope sigma typ - | WithoutTypeConstraint -> None + | WithoutTypeConstraint | UnknownIfTermOrType -> None + +let allowed_binder_kind_of_type_kind = function + | IsType -> Some AbsPi + | OfType _ | WithoutTypeConstraint -> Some AbsLambda + | UnknownIfTermOrType -> None let empty_ltac_sign = { ltac_vars = Id.Set.empty; @@ -2348,9 +2423,10 @@ let intern_gen kind env sigma ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind sigma kind in + let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; - impls; impl_binder_index = Some 0} + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2372,8 +2448,8 @@ let interp_gen kind env sigma ?(impls=empty_internalization_env) c = let c = intern_gen kind ~impls env sigma c in understand ~expected_type:kind env sigma c -let interp_constr env sigma ?(impls=empty_internalization_env) c = - interp_gen WithoutTypeConstraint env sigma c +let interp_constr ?(expected_type=WithoutTypeConstraint) env sigma ?(impls=empty_internalization_env) c = + interp_gen expected_type env sigma c let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c @@ -2383,8 +2459,8 @@ let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = (* Not all evars expected to be resolved *) -let interp_open_constr env sigma c = - understand_tcc env sigma (intern_constr env sigma c) +let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c = + understand_tcc env sigma (intern_gen expected_type env sigma c) (* Not all evars expected to be resolved and computation of implicit args *) @@ -2432,8 +2508,10 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = let tmp_scope = scope_of_type_kind sigma kind in let impls = empty_internalization_env in + let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0} + {ids; unb = false; tmp_scope; scopes = []; impls; + binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = @@ -2442,7 +2520,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = None} + {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} false (empty_ltac_sign, vl) a in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) @@ -2473,13 +2551,17 @@ let my_intern_constr env lvar acc c = let intern_context env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in + let ids = + (* We assume all ids around are parts of the prefix of the current + context being interpreted *) + extract_ids env in let lenv, bl = List.fold_left (fun (lenv, bl) b -> let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) - ({ids = extract_ids env; unb = false; + ({ids; unb = false; tmp_scope = None; scopes = []; impls = impl_env; - impl_binder_index = Some 0}, []) binders in + binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) @@ -2500,8 +2582,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let r = Retyping.relevance_of_type env sigma t in let d = LocalAssum (make_annot na r,t) in let impls = - if k == Implicit then CAst.make (Some (na,true)) :: impls - else CAst.make None :: impls + match k with + | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls + | MaxImplicit -> CAst.make (Some (na,true)) :: impls + | Explicit -> CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 8cce7cd9af..670563f02f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -97,7 +97,7 @@ val intern_context : env -> internalization_env -> local_binder_expr list -> int (** Main interpretation functions, using type class inference, expecting evars and pending problems to be all resolved *) -val interp_constr : env -> evar_map -> ?impls:internalization_env -> +val interp_constr : ?expected_type:typing_constraint -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> @@ -109,7 +109,7 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : ?expected_type:typing_constraint -> env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) diff --git a/interp/impargs.ml b/interp/impargs.ml index e2c732809a..9b50d9ca71 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -14,6 +14,7 @@ open Util open Names open Constr open Globnames +open Glob_term open Declarations open Lib open Libobject @@ -80,10 +81,24 @@ let with_implicit_protection f x = let () = implicit_args := oflags in iraise reraise -let set_maximality imps b = +type on_trailing_implicit = Error | Info | Silent + +let msg_trailing_implicit (fail : on_trailing_implicit) id = + let str1 = "Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, " in + match fail with + | Error -> + user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ].")) + | Info -> + Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted.")) + | Silent -> () + +let set_maximality fail id imps b = (* Force maximal insertion on ending implicits (compatibility) *) - let is_set x = match x with None -> false | _ -> true in - b || List.for_all is_set imps + b || ( + let is_set x = match x with None -> false | _ -> true in + let b' = List.for_all is_set imps in + if b' then msg_trailing_implicit fail id; + b') (*s Computation of implicit arguments *) @@ -302,6 +317,11 @@ let is_status_implicit = function let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k) +let binding_kind_of_status = function + | Some (_, _, (false, _)) -> NonMaxImplicit + | Some (_, _, (true, _)) -> MaxImplicit + | None -> Explicit + let name_of_implicit = function | None -> anomaly (Pp.str "Not an implicit argument.") | Some (ExplByName id,_,_) -> id @@ -340,19 +360,19 @@ let rec prepare_implicits f = function | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") | (Name id, Some imp)::imps -> let imps' = prepare_implicits f imps in - Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps' + Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let set_manual_implicits flags enriching autoimps l = +let set_manual_implicits silent flags enriching autoimps l = (* Compare with automatic implicits to recover printing data and names *) let rec merge k autoimps explimps = match autoimps, explimps with | autoimp::autoimps, explimp::explimps -> let imps' = merge (k+1) autoimps explimps in begin match autoimp, explimp.CAst.v with | (Name id,_), Some (_,max) -> - Some (ExplByName id, Manual, (set_maximality imps' max, true)) + Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true)) | (Name id,Some exp), None when enriching -> - Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true)) + Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true)) | (Name _,_), None -> None | (Anonymous,_), Some (Name id,max) -> Some (ExplByName id,Manual,(max,true)) @@ -497,8 +517,9 @@ let impls_of_context ctx = let map decl = let id = NamedDecl.get_id decl in match Id.Map.get id !sec_implicits with - | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true)) - | Glob_term.Explicit -> None + | NonMaxImplicit -> Some (ExplByName id, Manual, (false, true)) + | MaxImplicit -> Some (ExplByName id, Manual, (true, true)) + | Explicit -> None in List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx) @@ -608,7 +629,7 @@ type manual_implicits = (Name.t * bool) option CAst.t list let compute_implicits_with_manual env sigma typ enriching l = let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in - set_manual_implicits !implicit_args enriching autoimpls l + set_manual_implicits true !implicit_args enriching autoimpls l let check_inclusion l = (* Check strict inclusion *) @@ -636,7 +657,7 @@ let declare_manual_implicits local ref ?enriching l = let t = of_constr t in let enriching = Option.default flags.auto enriching in let autoimpls = compute_auto_implicits env sigma flags enriching t in - let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in + let l = [DefaultImpArgs, set_manual_implicits false flags enriching autoimpls l] in let req = if is_local local ref then ImplLocal else ImplInteractive(flags,ImplManual (List.length autoimpls)) @@ -647,22 +668,16 @@ let maybe_declare_manual_implicits local ref ?enriching l = declare_manual_implicits local ref ?enriching l -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 - let compute_implicit_statuses autoimps l = let rec aux i = function - | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, MaximallyImplicit :: manualimps -> + | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) + | Name id :: autoimps, MaxImplicit :: manualimps -> Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, Implicit :: manualimps -> + | Name id :: autoimps, NonMaxImplicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in - let max = set_maximality imps' false in - if max then msg_trailing_implicit id; + let max = set_maximality Error id imps' false in Some (ExplByName id, Manual, (max, true)) :: imps' - | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> + | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ -> user_err ~hdr:"set_implicits" (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit.")) | autoimps, [] -> List.map (fun _ -> None) autoimps @@ -684,7 +699,7 @@ let set_implicits local ref l = check_rigidity (is_rigid env sigma t); (* Sort by number of implicits, decreasing *) let is_implicit = function - | NotImplicit -> false + | Explicit -> false | _ -> true in let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in diff --git a/interp/impargs.mli b/interp/impargs.mli index ef3c2496f4..65e7fd8aaf 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -77,6 +77,7 @@ type implicit_side_condition type implicits_list = implicit_side_condition * implicit_status list val is_status_implicit : implicit_status -> bool +val binding_kind_of_status : implicit_status -> Glob_term.binding_kind val is_inferable_implicit : bool -> int -> implicit_status -> bool val name_of_implicit : implicit_status -> Id.t val maximal_insertion_of : implicit_status -> bool @@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits -> unit -type implicit_kind = Implicit | MaximallyImplicit | NotImplicit - (** [set_implicits local ref l] Manual declaration of implicit arguments. `l` is a list of possible sequences of implicit statuses. *) -val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit +val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit val implicits_of_global : GlobRef.t -> implicits_list list diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8b457ab37b..ffbb982ab7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -203,8 +203,9 @@ let warn_ignoring_implicit_status = let implicits_of_glob_constr ?(with_products=true) l = let add_impl ?loc na bk l = match bk with - | Implicit -> CAst.make ?loc (Some (na,true)) :: l - | _ -> CAst.make ?loc None :: l + | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l + | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l + | Explicit -> CAst.make ?loc None :: l in let rec aux c = match DAst.get c with @@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l = if with_products then add_impl na bk (aux b) else let () = match bk with - | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc - | _ -> () + | NonMaxImplicit + | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | Explicit -> () in [] | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) | GLetIn (na, b, t, c) -> aux c diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 265ca58ed9..d1eb50d370 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -151,6 +151,24 @@ let rec subst_glob_vars l gc = DAst.map (function let ldots_var = Id.of_string ".." +type 'a binder_status_fun = { + no : 'a -> 'a; + restart_prod : 'a -> 'a; + restart_lambda : 'a -> 'a; + switch_prod : 'a -> 'a; + switch_lambda : 'a -> 'a; + slide : 'a -> 'a; +} + +let default_binder_status_fun = { + no = (fun x -> x); + restart_prod = (fun x -> x); + restart_lambda = (fun x -> x); + switch_prod = (fun x -> x); + switch_lambda = (fun x -> x); + slide = (fun x -> x); +} + let protect g e na = let e',disjpat,na = g e na in if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); @@ -163,10 +181,10 @@ let apply_cases_pattern_term ?loc (ids,disjpat) tm c = let apply_cases_pattern ?loc (ids_disjpat,id) c = apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c -let glob_constr_of_notation_constr_with_binders ?loc g f e nc = +let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_status_fun) e nc = let lt x = DAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id - | NApp (a,args) -> GApp (f e a, List.map (f e) args) + | NApp (a,args) -> let e = h.no e in GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in @@ -180,15 +198,18 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> - let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) + let e = h.switch_lambda e in + let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NProd (na,ty,c) -> - let e',disjpat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) + let e = h.switch_prod e in + let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) | NLetIn (na,b,t,c) -> let e',disjpat,na = g e na in (match disjpat with - | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c) + | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c) | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> + let e = h.no e in let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None @@ -207,19 +228,22 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = List.map (fun patl -> CAst.make (idl,patl,f e rhs)) disjpatl) eqnl in GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl') | NLetTuple (nal,(na,po),b,c) -> + let e = h.no e in let e',nal = List.fold_left_map (protect g) e nal in let e'',na = protect g e na in GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c) | NIf (c,(na,po),b1,b2) -> + let e = h.no e in let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> + let e = h.no e in let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k) + | NCast (c,k) -> GCast (f e c,map_cast_type (f (h.slide e)) k) | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index f9de6b7d6b..c62dac013b 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -35,12 +35,21 @@ val notation_constr_of_glob_constr : notation_interp_env -> (** Re-interpret a notation as a [glob_constr], taking care of binders *) +type 'a binder_status_fun = { + no : 'a -> 'a; + restart_prod : 'a -> 'a; + restart_lambda : 'a -> 'a; + switch_prod : 'a -> 'a; + switch_lambda : 'a -> 'a; + slide : 'a -> 'a; +} + val apply_cases_pattern : ?loc:Loc.t -> (Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t -> ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) -> - ('a -> notation_constr -> glob_constr) -> + ('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun -> 'a -> notation_constr -> glob_constr val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_constr diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f1eb000c88..31dd26d2ba 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -258,17 +258,6 @@ let cook_constant { from = cb; info } = (********************************) (* Discharging mutual inductive *) -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 = @@ -305,7 +294,7 @@ let abstract_projection ~params expmod hyps t = 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 +let cook_one_ind ~ntypes (section_decls,_ as hyps) expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> @@ -314,7 +303,7 @@ let cook_one_ind ~template_check ~ntypes RegularArity {mind_user_arity=arity; mind_sort=sort} | TemplateArity {template_param_levels=levels;template_level;template_context} -> let sec_levels = CList.map_filter (fun d -> - if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d) + if RelDecl.is_local_assum d then Some None else None) section_decls in @@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = 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) + Array.map (cook_one_ind ~ntypes hyps expmod) mib.mind_packets in let mind_record = match mib.mind_record with diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c550b0d432..ac130d018d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -89,10 +89,6 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) - check_template : bool; - (* If [false] then we don't check that the universes template-polymorphic - inductive parameterize on are necessarily local and unbounded from below. - This potentially introduces inconsistencies. *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 047027984d..a3adac7a11 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,7 +26,6 @@ let safe_flags oracle = { enable_VM = true; enable_native_compiler = true; indices_matter = true; - check_template = true; } (** {6 Arities } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index f04863386f..87f2f234da 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter -let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound @@ -449,7 +448,6 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; - check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -458,8 +456,7 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler && - check_template == alt.check_template + enable_native_compiler == alt.enable_native_compiler [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -591,9 +588,6 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes -let template_checked_ind (mind,_i) env = - (lookup_mind mind env).mind_typing_flags.check_template - let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true @@ -802,14 +796,6 @@ let get_template_polymorphic_variables env r = | IndRef ind -> template_polymorphic_variables ind env | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env -let is_template_checked env r = - let open Names.GlobRef in - match r with - | VarRef _id -> false - | ConstRef _c -> false - | IndRef ind -> template_checked_ind ind env - | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env - let is_type_in_type env r = let open Names.GlobRef in match r with diff --git a/kernel/environ.mli b/kernel/environ.mli index bd5a000c2b..e80d0a9b9f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool -val check_template : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool @@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool val template_polymorphic_ind : inductive -> env -> bool val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool -val template_checked_ind : inductive -> env -> bool (** {5 Modules } *) @@ -373,7 +371,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list -val is_template_checked : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool (** Native compiler *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 113ee787f2..cc15109f06 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -197,7 +197,7 @@ let unbounded_from_below u cstrs = (starting from the most recent and ignoring let-definitions) is not contributing to the inductive type's sort or is Some u_k if its level is u_k and is contributing. *) -let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = +let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && @@ -205,27 +205,23 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc in let univs = Univ.Universe.levels concl in let univs = - if template_check then - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - else univs (* Doesn't check the universes can be generalized *) + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> - if template_check then (match Univ.Universe.level u with | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None | None -> None) - else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in params, univs -let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in @@ -267,9 +263,9 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp splayed_lc in let param_levels, concl_levels = - template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + template_polymorphic_univs ~ctor_levels ctx params min_univ in - if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + if List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") @@ -356,8 +352,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let template_check = Environ.check_template env in - let data = List.map (abstract_packets ~template_check univs usubst params) data in + let data = List.map (abstract_packets univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8dea8f046d..723ba5459e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option (* Utility function to compute the actual universe parameters of a template polymorphic inductive *) val template_polymorphic_univs : - template_check:bool -> ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> diff --git a/library/global.ml b/library/global.ml index fbbe09301b..8706238f5a 100644 --- a/library/global.ml +++ b/library/global.ml @@ -192,8 +192,6 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r -let is_template_checked r = is_template_checked (env ()) r - let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r let is_type_in_type r = is_type_in_type (env ()) r diff --git a/library/global.mli b/library/global.mli index b6bd69c17c..0198ac5952 100644 --- a/library/global.mli +++ b/library/global.mli @@ -150,7 +150,6 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool -val is_template_checked : GlobRef.t -> bool val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index af1e973261..dcc3a87b11 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -205,7 +205,7 @@ GRAMMAR EXTEND Gram | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> - { CAst.make ~loc @@ CGeneralization (Implicit, None, c) } + { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; @@ -431,17 +431,27 @@ GRAMMAR EXTEND Gram | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" -> { [CLocalDef (id,c,Some t)] } | "{"; id = name; "}" -> - { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" -> - { [CLocalAssum (id::idl,Default Implicit,c)] } + { [CLocalAssum (id::idl,Default MaxImplicit,c)] } | "{"; id = name; ":"; c = lconstr; "}" -> - { [CLocalAssum ([id],Default Implicit,c)] } + { [CLocalAssum ([id],Default MaxImplicit,c)] } | "{"; id = name; idl = LIST1 name; "}" -> - { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + | "["; id = name; "]" -> + { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" -> + { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] } + | "["; id = name; ":"; c = lconstr; "]" -> + { [CLocalAssum ([id],Default NonMaxImplicit,c)] } + | "["; id = name; idl = LIST1 name; "]" -> + { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc } + | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" -> + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> { let (p, ty) = match p.CAst.v with diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d8dbf2f3dc..b212e7046a 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -151,7 +151,7 @@ let declare_one_prenex_implicit locality f = with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> - Impargs.MaximallyImplicit :: loop args' + MaxImplicit :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 02c2fc4a13..0969b3cc03 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true - | Implicit, Implicit -> true - | (Explicit | Implicit), _ -> false + | NonMaxImplicit, NonMaxImplicit -> true + | MaxImplicit, MaxImplicit -> true + | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 44323441b6..485a19421d 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t type cases_pattern = [ `any ] cases_pattern_g -type binding_kind = Explicit | Implicit +type binding_kind = Explicit | MaxImplicit | NonMaxImplicit (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cb0c4868b5..2d98d48aa0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,7 @@ open Evarconv module NamedDecl = Context.Named.Declaration -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint let (!!) env = GlobEnv.env env @@ -1290,7 +1290,7 @@ let ise_pretype_gen flags env sigma lvar kind c = in let env = GlobEnv.make ~hypnaming env sigma lvar in let sigma', c', c'_ty = match kind with - | WithoutTypeConstraint -> + | WithoutTypeConstraint | UnknownIfTermOrType -> let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in sigma, j.uj_val, j.uj_type | OfType exptyp -> diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 18e416596e..ee57f690a1 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> val search_guard : ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = + | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *) + | IsType (** Necessarily a type *) + | OfType of types (** A term of the expected type *) + | WithoutTypeConstraint (** A term of unknown expected type *) type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 814b1b0a06..f9f46e1ceb 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -143,7 +143,8 @@ let tag_var = tag Tag.variable let pr_generalization bk ak c = let hd, tl = match bk with - | Implicit -> "{", "}" + | NonMaxImplicit -> "[", "]" + | MaxImplicit -> "{", "}" | Explicit -> "(", ")" in (* TODO: syntax Abstraction Kind *) str "`" ++ str hd ++ c ++ str tl @@ -324,12 +325,14 @@ let tag_var = tag Tag.variable let surround_impl k p = match k with | Explicit -> str"(" ++ p ++ str")" - | Implicit -> str"{" ++ p ++ str"}" + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> str"{" ++ p ++ str"}" let surround_implicit k p = match k with | Explicit -> p - | Implicit -> (str"{" ++ p ++ str"}") + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> (str"{" ++ p ++ str"}") let pr_binder many pr (nal,k,t) = match k with diff --git a/printing/printer.ml b/printing/printer.ml index 97e0528939..8af4d1d932 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -859,8 +859,6 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism - on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -880,13 +878,10 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 - | TemplatePolymorphic m1, TemplatePolymorphic m2 -> - MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 - | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -947,9 +942,6 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") - | TemplatePolymorphic m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ - strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in diff --git a/printing/printer.mli b/printing/printer.mli index 1d7a25cbb6..cd5151bd8f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -231,8 +231,6 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism - on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v deleted file mode 100644 index fbd9c8bcba..0000000000 --- a/test-suite/failure/Template.v +++ /dev/null @@ -1,28 +0,0 @@ - -Module TestUnsetTemplateCheck. - Unset Template Check. - - Section Foo. - - Context (A : Type). - - Definition cstr := nat : ltac:(let ty := type of A in exact ty). - - Inductive myind := - | cons : A -> myind. - End Foo. - - (* Can only succeed if no template check is performed *) - Check myind True : Prop. - - About myind. - - (* test discharge puts things in the right order (by using the - checker on the result) *) - Section S. - - Variables (A:Type) (a:A). - Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B. - End S. - -End TestUnsetTemplateCheck. diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index c142d28ebe..0a989646cf 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -61,3 +61,18 @@ H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 +File "stdin", line 101, characters 47-48: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 105, characters 36-37: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 106, characters 34-35: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 22-23: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 30-31: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 7f3b332d7d..610fa48c0c 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -90,3 +90,25 @@ apply H with (a:=a). (* test compliance with printing *) Abort. End A. + +Module B. + +(* Check valid/invalid implicit arguments *) +Definition f1 {x} (y:forall {x}, x=0) := x+0. +Definition f2 := (((fun x => 0):forall {x:nat}, nat), 0). +Definition f3 := fun {x} (y:forall {x}, x=0) => x+0. + +Definition g1 {x} := match x with true => fun {x:bool} => x | false => fun x:bool => x end. +(* TODO: do not ignore the implicit here *) +Definition g2 '(x,y) {z} := x+y+z. + +Definition h1 := fun x:nat => (fun {x} => x) 0. +Definition h2 := let g := forall {y}, y=0 in g. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Definition l1 := ∀ {x:nat} {y:nat}, x=0. + +End B. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index aeebc0f98b..839df99ea7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -219,8 +219,8 @@ Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. Module G. Generalizable Variables A R. Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. -Check exists_true `{Reflexive A R}, forall x, R x x. -Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +Check exists_true `(Reflexive A R), forall x, R x x. +Check exists_true x `(Reflexive A R) y, x+y=0 -> forall z, R z z. End G. (* Allows recursive patterns for binders to be associative on the left *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 43f88f42a5..f65696e464 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -4,11 +4,11 @@ Entry constr:myconstr is [ "6" RIGHTA [ ] | "5" RIGHTA - [ SELF; "+"; NEXT ] + [ SELF; "+"; NEXT ] | "4" RIGHTA - [ SELF; "*"; NEXT ] + [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v index de34e007d2..df729588f4 100644 --- a/test-suite/success/Generalization.v +++ b/test-suite/success/Generalization.v @@ -11,4 +11,10 @@ Admitted. Print a_eq_b. +Require Import Morphisms. +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True. +Admitted. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index b16e4a1186..e68040e4d4 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -1,3 +1,15 @@ + +Axiom foo : forall (x y z t : nat), nat. + +Arguments foo {_} _ [z] t. +Check (foo 1). +Arguments foo {_} _ {z} {t}. +Fail Arguments foo {_} _ [z] {t}. +Check (foo 1). + +Definition foo1 [m] n := n + m. +Check (foo1 1). + Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). @@ -33,3 +45,11 @@ Abort. Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A. Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P. + +Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'. +Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b. +Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b. + +Definition F (id: forall [A] [x : A], A) := id. +Definition G := let id := (fun [A] (x : A) => x) in id. +Fail Definition G' := let id := (fun {A} (x : A) => x) in id. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index ecaaedca53..668d765d83 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -114,9 +114,13 @@ Check h 0. Inductive I {A} (a:A) : forall {n:nat}, Prop := | C : I a (n:=0). +Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop := + | C' : I' a eq_refl. + Inductive I2 (x:=0) : Prop := - | C2 {p:nat} : p = 0 -> I2. -Check C2 eq_refl. + | C2 {p:nat} : p = 0 -> I2 + | C2' [p:nat] : p = 0 -> I2. +Check C2' eq_refl. Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := | C3 : I3 a (n:=0). @@ -147,6 +151,7 @@ Set Warnings "syntax". (* Miscellaneous tests *) Check let f := fun {x:nat} y => y=true in f false. +Check let f := fun [x:nat] y => y=true in f false. (* Isn't the name "arg_1" a bit fragile, here? *) @@ -157,3 +162,10 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0). Set Warnings "+syntax". Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)). Set Warnings "syntax". + + +Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0. +Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. +Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. +Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. +Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 745cf950b5..950c784325 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,9 +9,8 @@ (************************************************************************) open Format -open Coqdep_lexer -open Coqdep_common open Minisys +open Coqdep_common (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -29,47 +28,6 @@ open Minisys let option_sort = ref false -let warning_mult suf iter = - let tab = Hashtbl.create 151 in - let check f d = - begin try - let d' = Hashtbl.find tab f in - if (Filename.dirname (file_name f d)) - <> (Filename.dirname (file_name f d')) then begin - coqdep_warning "the file %s is defined twice!" (f ^ suf) - end - with Not_found -> () end; - Hashtbl.add tab f d - in - iter check - -let sort () = - let seen = Hashtbl.create 97 in - let rec loop file = - let file = canonize file in - if not (Hashtbl.mem seen file) then begin - Hashtbl.add seen file (); - let cin = open_in (file ^ ".v") in - let lb = Lexing.from_channel cin in - try - while true do - match coq_action lb with - | Require (from, sl) -> - List.iter - (fun s -> - match search_v_known ?from s with - | None -> () - | Some f -> loop f) - sl - | _ -> () - done - with Fin_fichier -> - close_in cin; - printf "%s%s " file !suffixe - end - in - List.iter (fun (name,_) -> loop name) !vAccu - let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; @@ -159,8 +117,6 @@ let coqdep () = List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; - warning_mult ".mli" iter_mli_known; - warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; if !option_c then mL_dependencies (); coq_dependencies (); diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index bd72a52adf..5ece595f13 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -125,8 +125,8 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, iter_ml_known, search_ml_known = mkknown () -let add_mli_known, iter_mli_known, search_mli_known = mkknown () +let add_ml_known, _, search_ml_known = mkknown () +let add_mli_known, _, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () @@ -616,3 +616,30 @@ let rec treat_file old_dirname old_name = | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) | _ -> ()) | _ -> () + +let sort () = + let seen = Hashtbl.create 97 in + let rec loop file = + let file = canonize file in + if not (Hashtbl.mem seen file) then begin + Hashtbl.add seen file (); + let cin = open_in (file ^ ".v") in + let lb = Lexing.from_channel cin in + try + while true do + match coq_action lb with + | Require (from, sl) -> + List.iter + (fun s -> + match search_v_known ?from s with + | None -> () + | Some f -> loop f) + sl + | _ -> () + done + with Fin_fichier -> + close_in cin; + printf "%s%s " file !suffixe + end + in + List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 96266b8e36..1820db4a1e 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -20,44 +20,34 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a twice.*) val find_dir_logpath: string -> string list +(** Options *) val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref - val write_vos : bool ref -(** output vos and vok dependencies *) +val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable - val option_dynlink : dynlink ref + val norec_dirs : StrSet.t ref -val suffixe : string ref + type dir = string option -val get_extension : string -> string list -> string * string -val basename_noext : string -> string +val treat_file : dir -> string -> unit + +(** ML-related manipulation *) val mlAccu : (string * string * dir) list ref val mliAccu : (string * dir) list ref val mllibAccu : (string * dir) list ref -val vAccu : (string * string) list ref -val addQueue : 'a list ref -> 'a -> unit val add_ml_known : string -> dir -> string -> unit -val iter_ml_known : (string -> dir -> unit) -> unit -val search_ml_known : string -> dir option val add_mli_known : string -> dir -> string -> unit -val iter_mli_known : (string -> dir -> unit) -> unit -val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit -val search_mllib_known : string -> dir option -val search_v_known : ?from:string list -> string list -> string option -val file_name : string -> string option -> string -val escape : string -> string -val canonize : string -> string val mL_dependencies : unit -> unit + val coq_dependencies : unit -> unit -val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit val add_coqlib_known : bool -> string -> string list -> string -> unit -val add_caml_known : string -> string list -> string -> unit + val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used @@ -73,5 +63,4 @@ val add_rec_dir_no_import : val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val treat_file : dir -> string -> unit -val error_cannot_parse : string -> int * int -> 'a +val sort : unit -> unit diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 7d919956e8..506a8dc5b0 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -32,10 +32,6 @@ let set_type_in_type () = let typing_flags = Environ.typing_flags (Global.env ()) in Global.set_typing_flags { typing_flags with Declarations.check_universes = false } -let set_no_template_check () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_template = false } - (******************************************************************************) type color = [`ON | `AUTO | `EMACS | `OFF] @@ -526,7 +522,6 @@ let parse_args ~help ~init arglist : t * string list = |"-list-tags" -> set_query oval PrintTags |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval - |"-no-template-check" -> set_no_template_check (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 051638d53c..6848862603 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -81,7 +81,6 @@ let print_usage_common co command = \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ -\n -no-template-check disable checking of universes constraints on universes parameterizing template polymorphic inductive types\ \n -mangle-names x mangle auto-generated names using prefix x\ \n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ \n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index dacef1cb18..9f92eba729 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -356,8 +356,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in - if not mind.mind_typing_flags.check_template then - let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu - else accu + accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/classes.ml b/vernac/classes.ml index 77bc4e4f8a..b92c9e9b71 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -510,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = - if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 15077298aa..9d43debb77 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags = let implicits = List.map (List.map snd) implicits in let implicits_specified = match implicits with - | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l + | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l | _ -> true in if implicits_specified && clear_implicits_flag then diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index 71effddf67..cbc5fc15e2 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -12,6 +12,6 @@ val vernac_arguments : section_local:bool -> Libnames.qualid Constrexpr.or_by_notation -> Vernacexpr.vernac_argument_status list - -> (Names.Name.t * Impargs.implicit_kind) list list + -> (Names.Name.t * Glob_term.binding_kind) list list -> Vernacexpr.arguments_modifier list -> unit diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 625ffb5a06..d97bf6724c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -270,7 +270,7 @@ let context ~poly l = | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in + let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *) name,b,t,impl) ctx in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8de1c69424..dce0a70f72 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -323,16 +323,15 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl = +let template_polymorphism_candidate ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in if not concltemplate then false - else if not template_check then true else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in let params, conclunivs = - IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu + IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu in not (Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -385,7 +384,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames List.fold_left (fun levels c -> add_levels c levels) param_levels ctypes in - template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl + template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in let template = match template with | Some template -> diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index cc104b3762..1286e4a5c3 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : template_check:bool - -> ctor_levels:Univ.LSet.t + : ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params +(** [template_polymorphism_candidate ~ctor_levels uctx params conclsort] is [true] iff an inductive with params [params], conclusion [conclsort] and universe levels appearing in the constructor arguments [ctor_levels] would be definable as template polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its - conclusion sort, if one is given. If the [template_check] flag is - false we just check that the conclusion sort is not small. *) + conclusion sort, if one is given. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3302231fd1..d0374bc4fa 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -16,7 +16,6 @@ open Util open Names open Glob_term open Vernacexpr -open Impargs open Constrexpr open Constrexpr_ops open Extend @@ -817,7 +816,7 @@ GRAMMAR EXTEND Gram { let name, recarg_like, notation_scope = item in [RealArg { name=name; recarg_like=recarg_like; notation_scope=notation_scope; - implicit_status = NotImplicit}] } + implicit_status = Explicit}] } | "/" -> { [VolatileArg] } | "&" -> { [BidiArg] } | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> @@ -827,7 +826,7 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = NotImplicit}) items } + implicit_status = Explicit}) items } | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x @@ -835,7 +834,7 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = Implicit}) items } + implicit_status = NonMaxImplicit}) items } | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x @@ -843,16 +842,16 @@ GRAMMAR EXTEND Gram List.map (fun (name,recarg_like,notation_scope) -> RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; - implicit_status = MaximallyImplicit}) items } + implicit_status = MaxImplicit}) items } ] ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> { [(name.CAst.v, NotImplicit)] } + [ name = name -> { [(name.CAst.v, Explicit)] } | "["; items = LIST1 name; "]" -> - { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items } + { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items } | "{"; items = LIST1 name; "}" -> - { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items } + { List.map (fun name -> (name.CAst.v, MaxImplicit)) items } ] ]; strategy_level: diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a1bd99c237..82132a1af6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1076,14 +1076,14 @@ let string_of_definition_object_kind = let open Decls in function let pr_br imp force x = let left,right = match imp with - | Impargs.Implicit -> str "[", str "]" - | Impargs.MaximallyImplicit -> str "{", str "}" - | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt() + | Glob_term.NonMaxImplicit -> str "[", str "]" + | Glob_term.MaxImplicit -> str "{", str "}" + | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt() in left ++ x ++ right in let get_arguments_like s imp tl = - if s = None && imp = Impargs.NotImplicit then [], tl + if s = None && imp = Glob_term.Explicit then [], tl else let rec fold extra = function | RealArg arg :: tl when diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 2cd1cf7c65..32c438c724 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -211,12 +211,10 @@ let pr_template_variables = function let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - let template_checked = Global.is_template_checked ref in let template_variables = Global.get_template_polymorphic_variables ref in [ pr_global ref ++ str " is " ++ (if poly then str "universe polymorphic" else if template_poly then - (if not template_checked then str "assumed " else mt()) ++ str "template universe polymorphic " ++ h 0 (pr_template_variables template_variables) else str "not universe polymorphic") ] @@ -260,18 +258,18 @@ let implicit_name_of_pos = function | Constrexpr.ExplByPos (n,k) -> Anonymous let implicit_kind_of_status = function - | None -> Anonymous, NotImplicit - | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit + | None -> Anonymous, Glob_term.Explicit + | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit let dummy = { - Vernacexpr.implicit_status = NotImplicit; + Vernacexpr.implicit_status = Glob_term.Explicit; name = Anonymous; recarg_like = false; notation_scope = None; } let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = - name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit let rec main_implicits i renames recargs scopes impls = if renames = [] && recargs = [] && scopes = [] && impls = [] then [] @@ -283,8 +281,8 @@ let rec main_implicits i renames recargs scopes impls = let (name, implicit_status) = match renames, impls with | _, (Some _ as i) :: _ -> implicit_kind_of_status i - | name::_, _ -> (name,NotImplicit) - | [], (None::_ | []) -> (Anonymous, NotImplicit) + | name::_, _ -> (name,Glob_term.Explicit) + | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit) in let notation_scope = match scopes with | scope :: _ -> Option.map CAst.make scope diff --git a/vernac/record.ml b/vernac/record.ml index df9b4a0914..f6945838d7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -446,8 +446,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa univs) param_levels fields in - let template_check = Environ.check_template (Global.env ()) in - ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params + ComInductive.template_polymorphism_candidate ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d011fb2e77..fd588f5b15 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -609,24 +609,6 @@ let vernac_assumption ~atts discharge kind l nl = | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l -let set_template_check b = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_template = b } - -let is_template_check () = - let typing_flags = Environ.typing_flags (Global.env ()) in - typing_flags.Declarations.check_template - -let () = - let tccheck = - { optdepr = true; - optname = "Template universe check"; - optkey = ["Template"; "Check"]; - optread = (fun () -> is_template_check ()); - optwrite = (fun b -> set_template_check b)} - in - declare_bool_option tccheck - let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false ~name:"Polymorphic inductive cumulativity" @@ -1589,7 +1571,7 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~pstate ~atts redexp glopt rc = let glopt = query_command_selector glopt in let sigma, env = get_current_context_of_args ~pstate glopt in - let sigma, c = interp_open_constr env sigma rc in + let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in Evarconv.check_problems_are_solved env sigma; let sigma = Evd.minimize_universes sigma in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 1daa244986..22a8de7f99 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -254,7 +254,7 @@ type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; - implicit_status : Impargs.implicit_kind; + implicit_status : Glob_term.binding_kind; } type vernac_argument_status = @@ -386,7 +386,7 @@ type nonrec vernac_expr = | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |